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.
cheers chris _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
