[isabelle] Synchronisation of thm, find_theorems, etc.
I have a large theory with many lemmas proved with single `by` commands. If I open this in
Isabelle/jEdit and start a new lemma at the bottom, I can start working on this interactively while
Isabelle continues to prove the above lemmas in parallel in the background. I can even use the
lemmas for which Isabelle has not yet processed the proof. This is very pleasant.
However, if I try to invoke something like `thm` or `find_theorems`, these appear to block until
processing reaches that point. Is there a reason for this? It seems surprising to me that I can use
a lemma, but cannot inspect it:
lemma foo: "..."
thm bar (* no output until serial processing reaches this point *)
apply bar (* works fine, even before the above line has been processed *)
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