# HG changeset patch
# User wenzelm
# Date 1271237071 -7200
# Node ID c210a8fda4c5a0c5c904377a643d498265c472f8
# Parent  1d199975ebf926036168da1c136465be3cd3a3af
updated Thm.add_axiom/add_def;

diff -r 1d199975ebf9 -r c210a8fda4c5 doc-src/IsarImplementation/Thy/Logic.thy
--- 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"} \\
diff -r 1d199975ebf9 -r c210a8fda4c5 doc-src/IsarImplementation/Thy/ML.thy
--- 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
diff -r 1d199975ebf9 -r c210a8fda4c5 doc-src/IsarImplementation/Thy/document/Logic.tex
--- 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| \\
diff -r 1d199975ebf9 -r c210a8fda4c5 doc-src/IsarImplementation/Thy/document/ML.tex
--- 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