*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] Latex / Isabelle (Beginner)*From*: Nemo <ncuriel at gmail.com>*Date*: Sat, 3 Dec 2011 11:30:42 -0800

Hello all, I am new to extracting Latex files from Isabelle files. I read the documentation but does not make sense to me. It says to use 'isabelle mkdir NAME', but where do I even type this in? A terminal? Isabelle? Within a file? Which? I'm so confused. Any help would be greatly appreciated. Thank you so much. Nemo Curiel

**Follow-Ups**:**Re: [isabelle] Latex / Isabelle (Beginner)***From:*Ramana Kumar

**Re: [isabelle] Latex / Isabelle (Beginner)***From:*James Frank

- Previous by Date: [isabelle] Fwd: Isabelle/HOL postdoc positions
- Next by Date: Re: [isabelle] Latex / Isabelle (Beginner)
- Previous by Thread: [isabelle] Fwd: Isabelle/HOL postdoc positions
- Next by Thread: Re: [isabelle] Latex / Isabelle (Beginner)
- Cl-isabelle-users December 2011 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