[isabelle] Why doesn't \<emptyset> work?



Looking in the Symbols panel under Unsorted, I see a lot of symbols that wouldn't make sense in Isabelle/Isar (flat, sharp, euros, pounds, etc.) but one that definitely would make sense, namely \<emptyset> (the zero with a slash through it). Isabelle does have notation for the empty set, namely {} (so for example {} union X is X; {} intersect X is {}; and these can be proved by simp) but these don't work if {} is replaced by the empty-set symbol, even though \<em does auto-complete to that symbol. Is there a good reason for this? If not, perhaps it could be fixed in the next version. (When I teach discrete mathematics, I always use that symbol instead of {} .)
--
Prof. W. Douglas Maurer                Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University       Fax  (1-202)994-4875


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.