[isabelle-dev] HOL iff notation

[Makarius]

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