--- a/doc-src/IsarImplementation/Thy/Logic.thy Wed Apr 14 11:11:23 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Wed Apr 14 11:24:31 2010 +0200
@@ -552,10 +552,10 @@
@{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
@{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
@{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
- @{index_ML Thm.add_axiom: "binding * term -> theory -> thm * theory"} \\
+ @{index_ML Thm.add_axiom: "binding * term -> theory -> (string * thm) * theory"} \\
@{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory
-> (string * ('a -> thm)) * theory"} \\
- @{index_ML Thm.add_def: "bool -> bool -> binding * term -> theory -> thm * theory"} \\
+ @{index_ML Thm.add_def: "bool -> bool -> binding * term -> theory -> (string * thm) * theory"} \\
\end{mldecls}
\begin{mldecls}
@{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
--- a/doc-src/IsarImplementation/Thy/ML.thy Wed Apr 14 11:11:23 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Wed Apr 14 11:24:31 2010 +0200
@@ -319,7 +319,7 @@
\smallskip\begin{mldecls}
@{ML "Sign.declare_const: (binding * typ) * mixfix
-> theory -> term * theory"} \\
- @{ML "Thm.add_def: bool -> bool -> binding * term -> theory -> thm * theory"}
+ @{ML "Thm.add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory"}
\end{mldecls}
\noindent Written with naive application, an addition of constant
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Apr 14 11:11:23 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Apr 14 11:24:31 2010 +0200
@@ -560,10 +560,10 @@
\indexdef{}{ML}{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
\indexdef{}{ML}{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
\indexdef{}{ML}{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
- \indexdef{}{ML}{Thm.add\_axiom}\verb|Thm.add_axiom: binding * term -> theory -> thm * theory| \\
+ \indexdef{}{ML}{Thm.add\_axiom}\verb|Thm.add_axiom: binding * term -> theory -> (string * thm) * theory| \\
\indexdef{}{ML}{Thm.add\_oracle}\verb|Thm.add_oracle: binding * ('a -> cterm) -> theory|\isasep\isanewline%
\verb| -> (string * ('a -> thm)) * theory| \\
- \indexdef{}{ML}{Thm.add\_def}\verb|Thm.add_def: bool -> bool -> binding * term -> theory -> thm * theory| \\
+ \indexdef{}{ML}{Thm.add\_def}\verb|Thm.add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory| \\
\end{mldecls}
\begin{mldecls}
\indexdef{}{ML}{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Wed Apr 14 11:11:23 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Wed Apr 14 11:24:31 2010 +0200
@@ -368,7 +368,7 @@
\smallskip\begin{mldecls}
\verb|Sign.declare_const: (binding * typ) * mixfix|\isasep\isanewline%
\verb| -> theory -> term * theory| \\
- \verb|Thm.add_def: bool -> bool -> binding * term -> theory -> thm * theory|
+ \verb|Thm.add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory|
\end{mldecls}
\noindent Written with naive application, an addition of constant