Re: [isabelle] Isabelle document preparation
Brian Huffman wrote:
One possible workaround would be to separate your assumptions using
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,
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