*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Easier quick PDF generation possible?*From*: Joachim Breitner <breitner at kit.edu>*Date*: Thu, 23 Oct 2014 13:44:43 +0200

Hi, I just create a small theory to do a quick experiment, and I wanted to share it with someone. Isabelle can create pretty PDF output, so I wanted to share it as such, but this turns out to be a task that is unnecessary complicated. Here is my log: 1. run "isabelle mkroot" 2. notice that I ran it wrong, "rm ROOT" 3. run "isabelle mkroot -d" 4. add my theory to ROOT, removed the theories [document = false] section, because empty sections are not allowed 5. run "isabelle build -D" 6. noticed that a few other theories were pulled in that I did not want 7. tried to add their theory names to the [document = false] section, for which I first had to look up the syntax in another ROOT file 8. noticed that this did not work. Put in the theory path (i.e. "~~/src/HOL/Library/Extended_Real") in there 9. adjusted document/root.txt to have a proper title and not disclose my local username Here is what I would have liked to do: 1. run "isabelle thy2pdf Foo.thy" So if anyone agrees that this would be useful, and is able to implement this minor feature suggestion, I’d appreciate that! Thanks, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Easier quick PDF generation possible?***From:*Andrew Butterfield

**Re: [isabelle] Easier quick PDF generation possible?***From:*Gergely Buday

- Previous by Date: [isabelle] proof terms & program extraction
- Next by Date: Re: [isabelle] Easier quick PDF generation possible?
- Previous by Thread: Re: [isabelle] proof terms & program extraction
- Next by Thread: Re: [isabelle] Easier quick PDF generation possible?
- Cl-isabelle-users October 2014 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