On Mon, 2 Sep 2013, Lawrence Paulson wrote:
I tend to use <->, but I'm afraid I don't know what a print mode is.
A print mode allows to change the way how the system prints things; there
are command line options -m MODE or Isabelle settings to various isabelle
tools for that.
Sometimes print modes have a genuine purpose, e.g. for different
"protocols" of the prover: Proof General, Isabelle Process, latex, HTML
etc.
Sometimes print modes are just there to allow everyone's favourite syntax
to coexist in the system. (The latter is an aspect of very old Isabelle
insider jokes that nobody remembers now.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
