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

On Sun, 11 Mar 2012, filip at matf.bg.ac.rs wrote:

(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?
`

`This is controlled by the print mode "iff". So for LaTeX document
``preparation, it should work via @{thm f_def [no_vars, mode = iff]}
`
You can also set Thy_Output.modes globally in your ROOT.ML file.

`It would be convenient if this could be done globally, so I could be
``sure that <-> is consistently used in the whole proof document.
`

`It will be consistent for printing, but source text is shown as you write
``it literally.
`

(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

See @{abbrev} as document antiquotation in the isar-ref manual.

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

`Raw == from Pure is mainly for foundational purposes, it is hardly ever
``used in Isabelle/HOL definitions these days.
`

`Things like 'definition' or 'inductive' or 'function' are all some derived
``form of theorems based on some primitive defs that the package
``implementations produce from the user input, and then recover the
``specified results by some mechanized proof. In contemporary Isabelle both
``'definition' and 'theorem' are non-trivial specification mechanisms in
``that sense.
`
Makarius

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