[isabelle-dev] print modes

[Brian Huffman]

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.

+1

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
later.

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