[isabelle-dev] HOL iff notation
makarius at sketis.net
Mon Sep 2 16:46:50 CEST 2013
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
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.)
More information about the isabelle-dev