*To*: "W. Douglas Maurer" <maurer at gwu.edu>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Why doesn't \<emptyset> work? (W. Douglas Maurer)*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 18 Feb 2015 07:31:32 +0100*In-reply-to*: <a06200751d10980831257@[192.168.1.20]>*References*: <a06200751d10980831257@[192.168.1.20]>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.4.0

Hi,

Hope this helps, Andreas On 18/02/15 00:51, W. Douglas Maurer wrote:

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.

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

- Previous by Date: Re: [isabelle] Why doesn't \<emptyset> work? (W. Douglas Maurer)
- Next by Date: Re: [isabelle] Local_Theory.map_naming in locales
- Previous by Thread: Re: [isabelle] Why doesn't \<emptyset> work? (W. Douglas Maurer)
- Next by Thread: Re: [isabelle] Why doesn't \<emptyset> work? (W. Douglas Maurer)
- 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