*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Generating .tex from .thy without a proper session*From*: Joachim Breitner <breitner at kit.edu>*Date*: Fri, 08 Feb 2013 11:33:26 +0100

Hi, while preparing some slides, I want to include some isabelle-generated LaTeX from a small fragment. So I fired up jEdit and wrote the few lines in Scratch.thy, saving that file to /tmp. Now I’d like to figure out how to convert that to .tex, without creating a full session and running "isabelle build" and then extracting the .tex from the generated .tex files. Is there a low-level-command that goes from .thy directly to .tex, without a session infrastructure involving ROOT and document/root.tex? I tried isabelle-process -I -q -m latex HOL < Scratch.thy which spits out LaTeX, but not the theory but rather the progress of processing it. Thanks, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:

- Previous by Date: Re: [isabelle] A way to write nested theories in a theory file?
- Next by Date: Re: [isabelle] Where to learn about HOL vs FOL?
- Previous by Thread: Re: [isabelle] Where to learn about the Mini-Haskell of the code generator?
- Next by Thread: Re: [isabelle] Generating .tex from .thy without a proper session
- Cl-isabelle-users February 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