# HG changeset patch
# User wenzelm
# Date 1287166781 -3600
# Node ID f4c614ece7eda648b53d13e8163459b1e4c87d7a
# Parent  b7b1a9e8f7c2c2f64756ce38ccf2ab0aae89319c
moved bind_thm(s) to implementation manual;

diff -r b7b1a9e8f7c2 -r f4c614ece7ed doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Thu Oct 14 21:55:21 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Fri Oct 15 19:19:41 2010 +0100
@@ -145,6 +145,8 @@
   \begin{mldecls}
   @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
   @{index_ML "Context.>> ": "(Context.generic -> Context.generic) -> unit"} \\
+  @{index_ML bind_thms: "string * thm list -> unit"} \\
+  @{index_ML bind_thm: "string * thm -> unit"} \\
   \end{mldecls}
 
   \begin{description}
@@ -158,6 +160,14 @@
   \item @{ML "Context.>>"}~@{text f} applies context transformation
   @{text f} to the implicit context of the ML toplevel.
 
+  \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
+  theorems produced in ML both in the (global) theory context and the
+  ML toplevel, associating it with the provided name.  Theorems are
+  put into a global ``standard'' format before being stored.
+
+  \item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a
+  singleton theorem.
+
   \end{description}
 
   It is very important to note that the above functions are really
diff -r b7b1a9e8f7c2 -r f4c614ece7ed doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Thu Oct 14 21:55:21 2010 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Fri Oct 15 19:19:41 2010 +0100
@@ -837,11 +837,6 @@
     @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 
-  \begin{mldecls}
-    @{index_ML bind_thms: "string * thm list -> unit"} \\
-    @{index_ML bind_thm: "string * thm -> unit"} \\
-  \end{mldecls}
-
   \begin{rail}
     'use' name
     ;
@@ -918,20 +913,6 @@
           let val context' = context
           in context' end)) *}  "my declaration"
 
-text {*
-  \begin{description}
-
-  \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
-  theorems produced in ML both in the theory context and the ML
-  toplevel, associating it with the provided name.  Theorems are put
-  into a global ``standard'' format before being stored.
-
-  \item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a
-  singleton theorem.
-  
-  \end{description}
-*}
-
 
 section {* Primitive specification elements *}
 
diff -r b7b1a9e8f7c2 -r f4c614ece7ed doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Thu Oct 14 21:55:21 2010 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Oct 15 19:19:41 2010 +0100
@@ -859,11 +859,6 @@
     \indexdef{}{command}{attribute\_setup}\hypertarget{command.attribute-setup}{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
   \end{matharray}
 
-  \begin{mldecls}
-    \indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
-    \indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
-  \end{mldecls}
-
   \begin{rail}
     'use' name
     ;
@@ -951,21 +946,6 @@
 %
 \endisadelimML
 %
-\begin{isamarkuptext}%
-\begin{description}
-
-  \item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of
-  theorems produced in ML both in the theory context and the ML
-  toplevel, associating it with the provided name.  Theorems are put
-  into a global ``standard'' format before being stored.
-
-  \item \verb|bind_thm| is similar to \verb|bind_thms| but refers to a
-  singleton theorem.
-  
-  \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsection{Primitive specification elements%
 }
 \isamarkuptrue%