IRC log for #isabelle, 2017-02-16

All times shown according to UTC.

Time Nick Message
02:14 chindy pruvisto: ah thanks
02:15 chindy is there something like \in but for lists so say, \forall x \in (A::'a list)
05:26 larsrh chindy: you can use the function "set" to convert a list to a set
10:38 silver joined #isabelle
15:57 JCaesar You can also define yourself a new abbreviation to do that. (I've always found this obnoxiousâ¦)
16:00 pruvisto but if you do so, it is probably a good idea to make it an input abbreviation
16:00 pruvisto i.e. abbreviation (input) "foo == â¦""
16:00 pruvisto otherwise, that abbreviation will also be used for printing
16:01 pruvisto which may confuse and/or annoy people who import your theories
20:15 _-___-_ joined #isabelle
20:15 _-___-_ left #isabelle