[isabelle-dev] HOL iff notation

Makarius 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 mailing list