doc-src/IsarImplementation/Thy/logic.thy
changeset 28290 4cc2b6046258
parent 28110 9d121b171a0a
child 28674 08a77c495dc1
     1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Sep 18 14:06:58 2008 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Sep 18 19:39:44 2008 +0200
     1.3 @@ -595,12 +595,12 @@
     1.4    @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
     1.5    @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
     1.6    @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
     1.7 -  @{index_ML Thm.invoke_oracle_i: "theory -> string -> theory * Object.T -> thm"} \\
     1.8 +  @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory
     1.9 +  -> (string * ('a -> thm)) * theory"} \\
    1.10    \end{mldecls}
    1.11    \begin{mldecls}
    1.12    @{index_ML Theory.add_axioms_i: "(string * term) list -> theory -> theory"} \\
    1.13    @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
    1.14 -  @{index_ML Theory.add_oracle: "string * (theory * Object.T -> term) -> theory -> theory"} \\
    1.15    @{index_ML Theory.add_defs_i: "bool -> bool -> (bstring * term) list -> theory -> theory"} \\
    1.16    \end{mldecls}
    1.17  
    1.18 @@ -651,16 +651,13 @@
    1.19    \item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named
    1.20    axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
    1.21  
    1.22 -  \item @{ML Thm.invoke_oracle_i}~@{text "thy name arg"} invokes a
    1.23 -  named oracle function, cf.\ @{text "axiom"} in
    1.24 -  \figref{fig:prim-rules}.
    1.25 +  \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named
    1.26 +  oracle rule, essentially generating arbitrary axioms on the fly,
    1.27 +  cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
    1.28  
    1.29    \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares
    1.30    arbitrary propositions as axioms.
    1.31  
    1.32 -  \item @{ML Theory.add_oracle}~@{text "(name, f)"} declares an oracle
    1.33 -  function for generating arbitrary axioms on the fly.
    1.34 -
    1.35    \item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
    1.36    \<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification
    1.37    for constant @{text "c\<^isub>\<tau>"}, relative to existing