# Re: [isabelle] Presenting theories - equality symbols and abbreviations

```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).
>