Re: [isabelle] Embeding theories in existing latex document

On Thu, 18 Jan 2007, Martin Kleberma wrote:

> i have a separate latex document where i want to present my theories, 
> and want to extract some of the definitions and proofs out of my 
> isabelle scripts and embed them into my document.
> Is this somehow possible.  I have only seen it the other way round 
> embedding latex code into the isabelle documents.

There are many ways to be creative here. First of all, see chapter 2 of 
the Isabelle System manual for basic explanations of the Isabelle document 
tool chain.  The default setup (e.g. the one produced via isatool mkdir) 
gives Isabelle most of the control.  Things can be easily adjusted, e.g. 
using the -D option for usedir to dump tex sources separately, potentially 
with -d false to disable Isabelle document processing.

While it is most natural to generate the main sources from Isabelle 
theories, afterwards it is up to root.tex to assemble all this, 
potentially with funny \input{MyTheory.tex} etc. in any way you like. 
Concerning the content, you may easily remap Isabelle symbols or tagged 
regions using LaTeX macros (see the documentation).

For the really creative user, Isabelle antiquotations written in ML 
(depending on the logical context!) may produce formal output quite 
easily.  (The LaTeX Sugar manual covers advanced use of existing 


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.