--- a/doc-src/IsarImplementation/Thy/document/logic.tex Thu Sep 18 19:39:44 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex Thu Sep 18 19:39:47 2008 +0200
@@ -593,12 +593,12 @@
\indexml{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
\indexml{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
\indexml{Thm.get\_axiom\_i}\verb|Thm.get_axiom_i: theory -> string -> thm| \\
- \indexml{Thm.invoke\_oracle\_i}\verb|Thm.invoke_oracle_i: theory -> string -> theory * Object.T -> thm| \\
+ \indexml{Thm.add\_oracle}\verb|Thm.add_oracle: bstring * ('a -> cterm) -> theory|\isasep\isanewline%
+\verb| -> (string * ('a -> thm)) * theory| \\
\end{mldecls}
\begin{mldecls}
\indexml{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (string * term) list -> theory -> theory| \\
\indexml{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
- \indexml{Theory.add\_oracle}\verb|Theory.add_oracle: string * (theory * Object.T -> term) -> theory -> theory| \\
\indexml{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory| \\
\end{mldecls}
@@ -646,16 +646,13 @@
\item \verb|Thm.get_axiom_i|~\isa{thy\ name} retrieves a named
axiom, cf.\ \isa{axiom} in \figref{fig:prim-rules}.
- \item \verb|Thm.invoke_oracle_i|~\isa{thy\ name\ arg} invokes a
- named oracle function, cf.\ \isa{axiom} in
- \figref{fig:prim-rules}.
+ \item \verb|Thm.add_oracle|~\isa{{\isacharparenleft}name{\isacharcomma}\ oracle{\isacharparenright}} produces a named
+ oracle rule, essentially generating arbitrary axioms on the fly,
+ cf.\ \isa{axiom} in \figref{fig:prim-rules}.
\item \verb|Theory.add_axioms_i|~\isa{{\isacharbrackleft}{\isacharparenleft}name{\isacharcomma}\ A{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares
arbitrary propositions as axioms.
- \item \verb|Theory.add_oracle|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}} declares an oracle
- function for generating arbitrary axioms on the fly.
-
\item \verb|Theory.add_deps|~\isa{name\ c\isactrlisub {\isasymtau}\ \isactrlvec d\isactrlisub {\isasymsigma}} declares dependencies of a named specification
for constant \isa{c\isactrlisub {\isasymtau}}, relative to existing
specifications for constants \isa{\isactrlvec d\isactrlisub {\isasymsigma}}.
--- a/doc-src/IsarRef/Thy/document/Spec.tex Thu Sep 18 19:39:44 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Thu Sep 18 19:39:47 2008 +0200
@@ -1135,8 +1135,8 @@
\indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isartrans{theory}{theory} \\
\end{matharray}
- The oracle interface promotes a given ML function \verb|theory -> T -> term| to \verb|theory -> T -> thm|, for some
- type \verb|T| given by the user. This acts like an infinitary
+ The oracle interface promotes a given ML function \verb|'a -> cterm|
+ to \verb|'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
@@ -1144,18 +1144,16 @@
that are not fully checked by Isabelle inferences.
\begin{rail}
- 'oracle' name '(' type ')' '=' text
+ 'oracle' name '=' text
;
\end{rail}
\begin{descr}
- \item [\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharparenleft}type{\isacharparenright}\ {\isacharequal}\ text{\isachardoublequote}}] turns the
- given ML expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type
- \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> term| into an
- ML function of type
- \verb|theory ->|~\isa{{\isachardoublequote}type{\isachardoublequote}}~\verb|-> thm|, which is
- bound to the global identifier \verb|name|.
+ \item [\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ text{\isachardoublequote}}] turns the given ML
+ expression \isa{{\isachardoublequote}text{\isachardoublequote}} of type \verb|'a -> cterm| into an
+ ML function of type \verb|'a -> thm|, which is bound to the
+ global identifier \verb|name|.
\end{descr}%
\end{isamarkuptext}%