*To*: "W. Douglas Maurer" <maurer at gwu.edu>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Why doesn't \<emptyset> work?*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sat, 14 Feb 2015 14:13:13 +0100*In-reply-to*: <a06200743d104bd3e9aec@[192.168.1.20]>*Organization*: TU Munich*References*: <a06200743d104bd3e9aec@[192.168.1.20]>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:31.0) Gecko/20100101 Thunderbird/31.4.0

Hi Douglas, Am 14.02.2015 um 10:26 schrieb W. Douglas Maurer: > 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 {} .) the answer is simple: there is no syntax to interpret \<emptyset> accordingly. You can add it using e.g. notation Set.empty ("\<emptyset> ") (untested, refer to the Isar reference manual for details). Hope this helps, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] Why doesn't \<emptyset> work?***From:*W. Douglas Maurer

- Previous by Date: Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014
- Next by Date: Re: [isabelle] Transfer Isabelle2011 Code to Isabelle2014
- Previous by Thread: [isabelle] Why doesn't \<emptyset> work?
- Next by Thread: Re: [isabelle] Why doesn't \<emptyset> work?
- Cl-isabelle-users February 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list