On Sun, 4 Mar 2012, Cezary Kaliszyk wrote:
Makarius once suggested an antiquotation, that does something like
'print_theorems'. I have not investigated how to implement one?
Pretty printing into latex source is not a big deal, if you are satisfied
with regular multiline output in the "display" style of the document
preparation system. If you are more ambitious, say you want some tabular
stuff in Latex, then some experts on LatexSugar and Christian Urban can
help.
Alternatively, the pretty printing can be done in plain HTML.
Yet more alternatively, you can just make an interactive print command,
say like 'print_theory'. In Isabelle/jEdit the target will be HTML
anyway.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
