# HG changeset patch
# User wenzelm
# Date 1121362092 -7200
# Node ID 9a6131627ea38f92d4cf4cc117e45504e143ff0b
# Parent  581764860c2b8387e7610e05f2b0d7c5e4c1db8b
improved 'oracle' command;

diff -r 581764860c2b -r 9a6131627ea3 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Thu Jul 14 17:21:35 2005 +0200
+++ b/doc-src/IsarRef/pure.tex	Thu Jul 14 19:28:12 2005 +0200
@@ -587,19 +587,23 @@
   \isarcmd{oracle} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 
-Oracles provide an interface to external reasoning systems, without giving up
-control completely --- each theorem carries a derivation object recording any
-oracle invocation.  See \cite[\S6]{isabelle-ref} for more information.
+The oracle interface promotes a given ML function \texttt{theory -> T -> term}
+to \texttt{theory -> T -> thm}, for some type \texttt{T} given by the user.
+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 ``\texttt{[!]}'' to indicate results that are not fully
+checked by Isabelle inferences.
 
 \begin{rail}
-  'oracle' name '=' text
+  'oracle' name '(' type ')' '=' text
   ;
 \end{rail}
 
 \begin{descr}
-\item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML
-  function $text$, which has to be of type
-  \texttt{Sign.sg~*~Object.T~->~term}.
+\item [$\isarkeyword{oracle}~name~(type)=~text$] turns the given ML expression
+  $text$ of type \texttt{theory~->~$type$~->~term} into an ML function $name$
+  of type \texttt{theory~->~$type$~->~thm}.
 \end{descr}