--- a/src/Doc/IsarImplementation/Logic.thy Mon Nov 19 18:01:48 2012 +0100
+++ b/src/Doc/IsarImplementation/Logic.thy Mon Nov 19 20:23:47 2012 +0100
@@ -648,6 +648,7 @@
\begin{mldecls}
@{index_ML_type thm} \\
@{index_ML proofs: "int Unsynchronized.ref"} \\
+ @{index_ML Thm.peek_status: "thm -> {oracle: bool, unfinished: bool, failed: bool}"} \\
@{index_ML Thm.transfer: "theory -> thm -> thm"} \\
@{index_ML Thm.assume: "cterm -> thm"} \\
@{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
@@ -670,6 +671,15 @@
\begin{description}
+ \item @{ML Thm.peek_status}~@{text "thm"} informs about the current
+ status of the derivation object behind the given theorem. This is a
+ snapshot of a potentially ongoing (parallel) evaluation of proofs.
+ The three Boolean values indicate the following: @{verbatim oracle}
+ if the finished part contains some oracle invocation; @{verbatim
+ unfinished} if some future proofs are still pending; @{verbatim
+ failed} if some future proof has failed, rendering the theorem
+ invalid!
+
\item @{ML Logic.all}~@{text "a B"} produces a Pure quantification
@{text "\<And>a. B"}, where occurrences of the atomic term @{text "a"} in
the body proposition @{text "B"} are replaced by bound variables.