src/Doc/IsarRef/Proof.thy
changeset 50126 3dec88149176
parent 50109 c13dc0b1841c
child 50772 6973b3f41334
     1.1 --- a/src/Doc/IsarRef/Proof.thy	Mon Nov 19 18:01:48 2012 +0100
     1.2 +++ b/src/Doc/IsarRef/Proof.thy	Mon Nov 19 20:23:47 2012 +0100
     1.3 @@ -670,9 +670,9 @@
     1.4    pretending to solve the pending claim without further ado.  This
     1.5    only works in interactive development, or if the @{ML
     1.6    quick_and_dirty} flag is enabled (in ML).  Facts emerging from fake
     1.7 -  proofs are not the real thing.  Internally, each theorem container
     1.8 -  is tainted by an oracle invocation, which is indicated as ``@{text
     1.9 -  "[!]"}'' in the printed result.
    1.10 +  proofs are not the real thing.  Internally, the derivation object is
    1.11 +  tainted by an oracle invocation, which may be inspected via the
    1.12 +  theorem status \cite{isabelle-implementation}.
    1.13    
    1.14    The most important application of @{command "sorry"} is to support
    1.15    experimentation and top-down proof development.