Re: [isabelle] Isabelle document preparation



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








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.