[isabelle-dev] print modes

Brian Huffman huffman at in.tum.de
Wed May 2 07:09:29 CEST 2012

On Wed, May 2, 2012 at 6:55 AM, Christian Sternagel
<c-sterna at jaist.ac.jp> wrote:
> 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.


I would actually go a bit further, and get rid of "xsymbol" as a
special syntax mode.

It bothers me that if I want to define a constant with both ascii and
symbol notation, I have to use the ascii variant in the actual
definition, and then add the (far more commonly-used) symbol notation

definition foo :: "'a => 'a => bool" (infix "~~" 50) where ...
notation (xsymbol) foo (infix "\<approx>" 50)

I would rather write:

definition foo :: "'a => 'a => bool" (infix "\<approx>" 50) where ...
notation (ascii) foo (infix "~~" 50)

- Brian

More information about the isabelle-dev mailing list