# Re: [isabelle] Why doesn't \<emptyset> work? (W. Douglas Maurer)

`After receiving Florian Haftmann's helpful response to my problem
``with \<emptyset>, I decided to try to extend this to be able to work
``with \<int> (the Z in a special font that means the set of all
``integers). There is a button for this under Letter in the Symbols
``pane. Accordingly, just like the use of notation Set.empty
``("\<emptyset>"), I tried notation Int.int ("\<int>"). The \<int> came
``out properly on the screen as the Z in a special font. Then I tried
``using it. If I write lemma "(a<(b::int))\Longrightarrow (a+c<b+c) by
``simp, that works. But if I substitute \<int> for int in the above,
``then \<int> again comes out on the screen as the Z in a special font,
``but the proof doesn't go through. I tried replacing Int.int in the
``notation statement by just int, but that doesn't work either. I
``suspect that there is something wrong with Int.int, but I don't know
``what syntax to try next.
`--
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.*