*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Isabelle document preparation*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Thu, 22 Jan 2009 08:37:18 -0800*In-reply-to*: <49789B31.3080808@uni-muenster.de>*References*: <49789B31.3080808@uni-muenster.de>*User-agent*: Internet Messaging Program (IMP) H3 (4.1.6)

Hi Peter, One possible workaround would be to separate your assumptions using "and": lemma assumes "P x" and "f x" However, if you are using named assumptions, this may cause problems. For example, with assumes A: "P x" "f x" the local theorem "A" refers to the list of both assumptions, while with assumes A: "P x" and "f x" the local theorem "A" refers only to "P x". Hope this helps, - Brian Quoting Peter Lammich <peter.lammich at uni-muenster.de>:

Hi all, I have a problem with the latex-document generated by Isabelle. No space is put in between inner-syntax blocks, i.e. if I have the following: lemma assumes "P x" "f x" it will look in latex like: lemma assumes P x f x That can be very confusing! Is there some tuning option to put some extra space, or perhaps a ";\ \ " in between such lists. The only workaround I know up to now is to put each such inner-syntax block in its own line, what makes the proofs more unreadable at editing time. Best and thanks for any hints, Peter

**Follow-Ups**:**Re: [isabelle] Isabelle document preparation***From:*Peter Lammich

**References**:**[isabelle] Isabelle document preparation***From:*Peter Lammich

- Previous by Date: [isabelle] Isabelle document preparation
- Next by Date: Re: [isabelle] Isabelle document preparation
- Previous by Thread: [isabelle] Isabelle document preparation
- Next by Thread: Re: [isabelle] Isabelle document preparation
- Cl-isabelle-users January 2009 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