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

You can unify your definitions (recursive or not) by always using "="
instead of "==".
Tobias
Am 11/03/2012 08:14, schrieb filip at matf.bg.ac.rs:
> (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
>

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*