doc-src/IsarImplementation/Thy/logic.thy
changeset 28674 08a77c495dc1
parent 28290 4cc2b6046258
child 28784 9495aec512e2
     1.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Thu Oct 23 14:22:16 2008 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Thu Oct 23 15:28:01 2008 +0200
     1.3 @@ -594,7 +594,7 @@
     1.4    @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
     1.5    @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
     1.6    @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
     1.7 -  @{index_ML Thm.get_axiom_i: "theory -> string -> thm"} \\
     1.8 +  @{index_ML Thm.axiom: "theory -> string -> thm"} \\
     1.9    @{index_ML Thm.add_oracle: "bstring * ('a -> cterm) -> theory
    1.10    -> (string * ('a -> thm)) * theory"} \\
    1.11    \end{mldecls}
    1.12 @@ -648,7 +648,7 @@
    1.13    term variables.  Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
    1.14    refer to the instantiated versions.
    1.15  
    1.16 -  \item @{ML Thm.get_axiom_i}~@{text "thy name"} retrieves a named
    1.17 +  \item @{ML Thm.axiom}~@{text "thy name"} retrieves a named
    1.18    axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
    1.19  
    1.20    \item @{ML Thm.add_oracle}~@{text "(name, oracle)"} produces a named