Email Gateway (Aug 22 2022 at 10:34): Email Gateway (Aug 22 2022 at 10:34):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
Hi all,
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 *)
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.
Last updated: Apr 20 2024 at 08:16 UTC