*To*: filip at matf.bg.ac.rs*Subject*: Re: [isabelle] Presenting theories - equality symbols and abbreviations*From*: John Wickerson <jpw48 at cam.ac.uk>*Date*: Sun, 11 Mar 2012 08:13:20 +0000*Cc*: isabelle-users Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <bded9cd871e4db7af10aea3cb8113ece.squirrel@webmail.matf.bg.ac.rs>*References*: <bded9cd871e4db7af10aea3cb8113ece.squirrel@webmail.matf.bg.ac.rs>

Hello Filip, With regard to your third question: I think "definition" and "fun" are rather different, so it makes sense to have different "==" and "=" symbols. > definition f where "f x == (x <-> True)" just means "define f as the function taking x to (x <-> True)", but > fun f where "f x = (x <-> True)" allows "f" to appear recursively on the RHS too, so it means "define f as the least fixed point of the equality f x = (x <-> True)". John On 11 Mar 2012, at 07:14, filip at matf.bg.ac.rs wrote: > Hello, > I am trying to generate LaTeX-ed proof documents from my Isabelle/HOL > theories and I have several technical questions. > > (1) Suppose I have a definition like > > definition f where "f x == x <-> True" > > When I use @{thm f_def[no_vars]}, in LaTeX, I get > > f x == x = True > > So, = is printed, although I used the <-> symbol. Is there a way to > persuade the system to print <-> for equality on bool type? It would be > convenient if this could be done globally, so I could be sure that <-> is > consistently used in the whole proof document. > > (2) If f is an abbreviation like > > abbreviation f where "f x == x <-> True" > > Is there a way to print it later using some antiquotation (as I used @{thm > f_def[no_vars]}, when f was a definition). > > (3) I noticed that function definitions do not allow using == but only =. > For example, I am not allowed to write: > > fun f where "f (a, b) == a > b" > > but only > > fun f where "f (a, b) = (a > b)" > > That seems a bit inconsistent with definitions made by using the > definition keyword. Is it maybe somehow possible to make @{thm > f.simps[no_vars]} print == instead of = so in LaTeX I get > > f (a, b) == a > b > > I prefer this notation (since it emphasizes that something holds by > definition, since it does not require additional parentheses and since it > is consistent with definitions given using the definition keyword). > > Thank you very much for your answers! > Filip > >

**References**:

- Previous by Date: [isabelle] Presenting theories - equality symbols and abbreviations
- Next by Date: Re: [isabelle] Presenting theories - equality symbols and abbreviations
- Previous by Thread: [isabelle] Presenting theories - equality symbols and abbreviations
- Next by Thread: Re: [isabelle] Presenting theories - equality symbols and abbreviations
- Cl-isabelle-users March 2012 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