[isabelle] Parallelising apply-style proofs



Hello all,

When working in Isabelle/jEdit with parallel proofs set to 2, "by" does not impede progress through
the theory. By which I mean a "by" step can remain purple and being processed while the rest of the
theory proceeds. The same does not seem to be true of a proof with many "apply" steps followed by a
"done." Is there a fundamental reason this doesn't happen or is this just a design decision? It
seems to me that processing could proceed past the proof as soon as the lemma statement itself has
been parsed.

This isn't a complaint as I realise there are several potential work arounds for this like using an
Isar proof or enabling skip proofs. I was just curious why this doesn't happen.

Thanks,
Matt

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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