[isabelle-dev] [isabelle] Status of HOL/Import

[Makarius]

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