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

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>

You can add it using e.g.

notation Set.empty ("\<emptyset> ")

(untested, refer to the Isar reference manual for details).

Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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