1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:38:02 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:38:44 2008 +0100
     1.3 @@ -1133,19 +1133,25 @@
     1.4  
     1.5  section {* Oracles *}
     1.6  
     1.7 -text {*
     1.8 +text {* Oracles allow Isabelle to take advantage of external reasoners
     1.9 +  such as arithmetic decision procedures, model checkers, fast
    1.10 +  tautology checkers or computer algebra systems.  Invoked as an
    1.11 +  oracle, an external reasoner can create arbitrary Isabelle theorems.
    1.12 +
    1.13 +  It is the responsibility of the user to ensure that the external
    1.14 +  reasoner is as trustworthy as the application requires.  Another
    1.15 +  typical source of errors is the linkup between Isabelle and the
    1.16 +  external tool, not just its concrete implementation, but also the
    1.17 +  required translation between two different logical environments.
    1.18 +
    1.19 +  Isabelle merely guarantees well-formedness of the propositions being
    1.20 +  asserted, and records within the internal derivation object how
    1.21 +  presumed theorems depend on unproven suppositions.
    1.22 +
    1.23    \begin{matharray}{rcl}
    1.24      @{command_def "oracle"} & : & \isartrans{theory}{theory} \\
    1.25    \end{matharray}
    1.26  
    1.27 -  The oracle interface promotes a given ML function @{ML_text "'a -> cterm"}
    1.28 -  to @{ML_text "'a -> thm"}.  This acts like an infinitary
    1.29 -  specification of axioms -- there is no internal check of the
    1.30 -  correctness of the results!  The inference kernel records oracle
    1.31 -  invocations within the internal derivation object of theorems, and
    1.32 -  the pretty printer attaches ``@{text "[!]"}'' to indicate results
    1.33 -  that are not fully checked by Isabelle inferences.
    1.34 -
    1.35    \begin{rail}
    1.36      'oracle' name '=' text
    1.37      ;
    1.38 @@ -1156,9 +1162,15 @@
    1.39    \item [@{command "oracle"}~@{text "name = text"}] turns the given ML
    1.40    expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
    1.41    ML function of type @{ML_text "'a -> thm"}, which is bound to the
    1.42 -  global identifier @{ML_text name}.
    1.43 +  global identifier @{ML_text name}.  This acts like an infinitary
    1.44 +  specification of axioms!  Invoking the oracle only works within the
    1.45 +  scope of the resulting theory.
    1.46  
    1.47    \end{descr}
    1.48 +
    1.49 +  See @{"file" "~~/src/FOL/ex/IffOracle.thy"} for a worked example of
    1.50 +  defining a new primitive rule as oracle, and turning it into a proof
    1.51 +  method.
    1.52  *}
    1.53  
    1.54  
    1.55 @@ -1201,7 +1213,7 @@
    1.56    (unqualified) names may never be hidden.
    1.57    
    1.58    Note that hiding name space accesses has no impact on logical
    1.59 -  declarations -- they remain valid internally.  Entities that are no
    1.60 +  declarations --- they remain valid internally.  Entities that are no
    1.61    longer accessible to the user are printed with the special qualifier
    1.62    ``@{text "??"}'' prefixed to the full internal name.
    1.63