Re: [isabelle] Isabelle document preparation



Brian Huffman wrote:
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.

I am using named assumptions in most cases, I'm afraid, so this is
   no option for me, as I would have to change too many existing proofs.

Moreover, I have a large base of existing proof scripts, so any automatic solution with
 as few changes to the scripts as possible would be the best.

Many thanks for the hint,
 Peter

p.s. At this point, I'm thinking about running a script over my .thy - files to put all those assumptions in separate lines, each. However, I think, this will make the proofs less readable in PG.








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