src/Doc/IsarImplementation/Logic.thy
 changeset 50126 3dec88149176 parent 48985 5386df44a037 child 52406 1e57c3c4e05c
     1.1 --- a/src/Doc/IsarImplementation/Logic.thy	Mon Nov 19 18:01:48 2012 +0100
1.2 +++ b/src/Doc/IsarImplementation/Logic.thy	Mon Nov 19 20:23:47 2012 +0100
1.3 @@ -648,6 +648,7 @@
1.4    \begin{mldecls}
1.5    @{index_ML_type thm} \\
1.6    @{index_ML proofs: "int Unsynchronized.ref"} \\
1.7 +  @{index_ML Thm.peek_status: "thm -> {oracle: bool, unfinished: bool, failed: bool}"} \\
1.8    @{index_ML Thm.transfer: "theory -> thm -> thm"} \\
1.9    @{index_ML Thm.assume: "cterm -> thm"} \\
1.10    @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
1.11 @@ -670,6 +671,15 @@
1.12
1.13    \begin{description}
1.14
1.15 +  \item @{ML Thm.peek_status}~@{text "thm"} informs about the current
1.16 +  status of the derivation object behind the given theorem.  This is a
1.17 +  snapshot of a potentially ongoing (parallel) evaluation of proofs.
1.18 +  The three Boolean values indicate the following: @{verbatim oracle}
1.19 +  if the finished part contains some oracle invocation; @{verbatim
1.20 +  unfinished} if some future proofs are still pending; @{verbatim
1.21 +  failed} if some future proof has failed, rendering the theorem
1.22 +  invalid!
1.23 +
1.24    \item @{ML Logic.all}~@{text "a B"} produces a Pure quantification
1.25    @{text "\<And>a. B"}, where occurrences of the atomic term @{text "a"} in
1.26    the body proposition @{text "B"} are replaced by bound variables.