# HG changeset patch
# User wenzelm
# Date 1226608724 -3600
# Node ID 529798e7192404653504ef9ec91b61fba1edcacc
# Parent  d5c1b7d67ea9a77b45d6e97d06f8b3ccd6210095
tuned section "Oracles";

diff -r d5c1b7d67ea9 -r 529798e71924 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:38:02 2008 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:38:44 2008 +0100
@@ -1133,19 +1133,25 @@
 
 section {* Oracles *}
 
-text {*
+text {* Oracles allow Isabelle to take advantage of external reasoners
+  such as arithmetic decision procedures, model checkers, fast
+  tautology checkers or computer algebra systems.  Invoked as an
+  oracle, an external reasoner can create arbitrary Isabelle theorems.
+
+  It is the responsibility of the user to ensure that the external
+  reasoner is as trustworthy as the application requires.  Another
+  typical source of errors is the linkup between Isabelle and the
+  external tool, not just its concrete implementation, but also the
+  required translation between two different logical environments.
+
+  Isabelle merely guarantees well-formedness of the propositions being
+  asserted, and records within the internal derivation object how
+  presumed theorems depend on unproven suppositions.
+
   \begin{matharray}{rcl}
     @{command_def "oracle"} & : & \isartrans{theory}{theory} \\
   \end{matharray}
 
-  The oracle interface promotes a given ML function @{ML_text "'a -> cterm"}
-  to @{ML_text "'a -> thm"}.  This acts like an infinitary
-  specification of axioms -- there is no internal check of the
-  correctness of the results!  The inference kernel records oracle
-  invocations within the internal derivation object of theorems, and
-  the pretty printer attaches ``@{text "[!]"}'' to indicate results
-  that are not fully checked by Isabelle inferences.
-
   \begin{rail}
     'oracle' name '=' text
     ;
@@ -1156,9 +1162,15 @@
   \item [@{command "oracle"}~@{text "name = text"}] turns the given ML
   expression @{text "text"} of type @{ML_text "'a -> cterm"} into an
   ML function of type @{ML_text "'a -> thm"}, which is bound to the
-  global identifier @{ML_text name}.
+  global identifier @{ML_text name}.  This acts like an infinitary
+  specification of axioms!  Invoking the oracle only works within the
+  scope of the resulting theory.
 
   \end{descr}
+
+  See @{"file" "~~/src/FOL/ex/IffOracle.thy"} for a worked example of
+  defining a new primitive rule as oracle, and turning it into a proof
+  method.
 *}
 
 
@@ -1201,7 +1213,7 @@
   (unqualified) names may never be hidden.
   
   Note that hiding name space accesses has no impact on logical
-  declarations -- they remain valid internally.  Entities that are no
+  declarations --- they remain valid internally.  Entities that are no
   longer accessible to the user are printed with the special qualifier
   ``@{text "??"}'' prefixed to the full internal name.