On Wed, May 2, 2012 at 6:55 AM, Christian Sternagel <[email protected]> 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
