doc-src/IsarImplementation/Thy/document/logic.tex

   \indexml{Thm.implies\_intr}\verb|Thm.implies_intr: cterm -> thm -> thm| \\
   \indexml{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
   \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}
 
   \begin{description}
 

   refer to the instantiated versions.
 
   \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}}.