--- 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
--- 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 *}
--- 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%