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.