# HG changeset patch
# User wenzelm
# Date 1226608830 -3600
# Node ID 4ce896a30f8860ca2a103a85df9c1b127203e984
# Parent  7f7002ad6289978ca5d113822d28e1218604ce11
added bind_thm, bind_thms;

diff -r 7f7002ad6289 -r 4ce896a30f88 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:40:00 2008 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:40:30 2008 +0100
@@ -808,6 +808,8 @@
     @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\
     @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\
     @{command_def "setup"} & : & \isartrans{theory}{theory} \\
+    @{index_ML bind_thms: "string * thm list -> unit"} \\
+    @{index_ML bind_thm: "string * thm -> unit"} \\
   \end{matharray}
 
   \begin{rail}
@@ -852,6 +854,14 @@
   of type @{ML_type [source=false] "theory -> theory"}.  This enables
   to initialize any object-logic specific tools and packages written
   in ML, for example.
+
+  \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{descr}
 *}
diff -r 7f7002ad6289 -r 4ce896a30f88 doc-src/IsarRef/style.sty
--- a/doc-src/IsarRef/style.sty	Thu Nov 13 21:40:00 2008 +0100
+++ b/doc-src/IsarRef/style.sty	Thu Nov 13 21:40:30 2008 +0100
@@ -16,6 +16,13 @@
 \newcommand{\figref}[1]{figure~\ref{#1}}
 \newcommand{\Figref}[1]{Figure~\ref{#1}}
 
+%% index
+\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
+\newcommand{\indexmlexception}[1]{\index{\emph{#1} (exception)|bold}}
+\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
+\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
+\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
+
 %% math
 \newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
 \renewcommand{\isadigit}[1]{\isamath{#1}}