[isabelle-dev] print modes
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)
More information about the isabelle-dev