[isabelle] Presenting theories - equality symbols and abbreviations



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






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