[isabelle-dev] [isabelle] Status of HOL/Import
makarius at sketis.net
Sun Mar 4 20:05:28 CET 2012
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
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
More information about the isabelle-dev