*To*: Nemo <ncuriel at gmail.com>*Subject*: Re: [isabelle] Latex / Isabelle (Beginner)*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Sun, 4 Dec 2011 09:35:27 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAEvpNU1VKeN-AgJMMxvNGAN=OXSLN906+VTO7y=QeiKKAQ9ToQ@mail.gmail.com>*References*: <CAEvpNU1VKeN-AgJMMxvNGAN=OXSLN906+VTO7y=QeiKKAQ9ToQ@mail.gmail.com>*Sender*: ramana.kumar at gmail.com

On Sat, Dec 3, 2011 at 7:30 PM, Nemo <ncuriel at gmail.com> wrote: > 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 believe you should type that in a terminal. > I'm so confused. > > Any help would be greatly appreciated. > > Thank you so much. > > Nemo Curiel

**References**:**[isabelle] Latex / Isabelle (Beginner)***From:*Nemo

- Previous by Date: [isabelle] Latex / Isabelle (Beginner)
- Next by Date: Re: [isabelle] Latex / Isabelle (Beginner)
- Previous by Thread: [isabelle] Latex / Isabelle (Beginner)
- 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