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

Makarius 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 mailing list