On 09/23/2010 04:03 PM, Makarius wrote:
[...]
The standard way to do that is via the wrapper Print_Mode.setmp [] --
as can be glimpsed from various existing examples in the sources.
Thank you for the hint above, and also for the notes below (now these
are just in time ;-)
Further notes on contemporary Isabelle/ML coding style:
* "term2str" is non-conventional, use term_to_string or string_of_term
or similar;
* "trm" is non-conventional, even though the Urban tutorial claims it
is, use t or tm or similar;
* function "theory" is very old style, use @{theory} antiquotation.
Makarius
Walther
_______________________________________________
Isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
