improved 'oracle' command;
Thu, 14 Jul 2005 19:28:12 +0200
changeset 16829 9a6131627ea3
parent 16828 581764860c2b
child 16830 5a2a600e0063
improved 'oracle' command;
--- 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} \\
-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.
-  'oracle' name '=' text
+  'oracle' name '(' type ')' '=' text
-\item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML
-  function $text$, which has to be of type
-  \texttt{*~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}.