[isabelle-dev] print modes

Christian Sternagel c-sterna at jaist.ac.jp
Wed May 2 06:55:23 CEST 2012

Dear all,

is it really the case that currently the only way to obtain ASCII output 
using print modes is by specifying the empty string, like

thm ("") conjE

or did I miss anything? Since this print mode is occasionally useful, I 
suggest to provide a named variant, like 'plain', 'ASCII', or whatever.



More information about the isabelle-dev mailing list