--- 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}}.