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

I posted a message entitled "Why doesn't \<emptyset> work?" (message 5, Sat, 14 Feb 2015). Then Florian Haftmann replied to me privately, saying: "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)." I tested that, and it does work. Thanks! (I still think it should be built in, though.)
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.