*To*: Joachim Breitner <breitner at kit.edu>*Subject*: Re: [isabelle] Latex without proofs*From*: Makarius <makarius at sketis.net>*Date*: Mon, 24 Jun 2013 16:13:22 +0200 (CEST)*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1372081567.4131.76.camel@kirk>*References*: <51C47AA8.9090506@inf.ethz.ch> <20130622084204.GA4827@hbl-lap-dell> <alpine.LNX.2.00.1306241439520.25726@macbroy21.informatik.tu-muenchen.de> <1372081567.4131.76.camel@kirk>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 24 Jun 2013, Joachim Breitner wrote:

Am Montag, den 24.06.2013, 14:46 +0200 schrieb Makarius:At some point I also hope to see document preparation as part of the Prover IDE. Only nostalgy associates latex documents with some batch build job, there are no particular technical reasons (apart from historical legacy getting in the way as usual).does this mean that in the future it will not be possible to have a script or makefile that will, say, create Isabelle course task and solutions PDFs from Isabelle sources automatically and without firing up a GUI program? Or are you merely stating that batch builds should not be the _only_ way to create documents from Isabelle sources?

Makarius

**References**:**[isabelle] Latex without proofs***From:*Stephan van Staden

**Re: [isabelle] Latex without proofs***From:*Holger Blasum

**Re: [isabelle] Latex without proofs***From:*Makarius

**Re: [isabelle] Latex without proofs***From:*Joachim Breitner

- Previous by Date: Re: [isabelle] Latex without proofs
- Next by Date: Re: [isabelle] Efficient_Nat and Imperative-HOL, strange import-order dependent bug
- Previous by Thread: Re: [isabelle] Latex without proofs
- Next by Thread: Re: [isabelle] obtains and is-bindings
- Cl-isabelle-users June 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list