[isabelle] Synchronisation of thm, find_theorems, etc.



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.




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