# [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.*