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.