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.