1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:40:00 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Nov 13 21:40:30 2008 +0100
     1.3 @@ -808,6 +808,8 @@
     1.4      @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\
     1.5      @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\
     1.6      @{command_def "setup"} & : & \isartrans{theory}{theory} \\
     1.7 +    @{index_ML bind_thms: "string * thm list -> unit"} \\
     1.8 +    @{index_ML bind_thm: "string * thm -> unit"} \\
     1.9    \end{matharray}
    1.10  
    1.11    \begin{rail}
    1.12 @@ -852,6 +854,14 @@
    1.13    of type @{ML_type [source=false] "theory -> theory"}.  This enables
    1.14    to initialize any object-logic specific tools and packages written
    1.15    in ML, for example.
    1.16 +
    1.17 +  \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
    1.18 +  theorems produced in ML both in the theory context and the ML
    1.19 +  toplevel, associating it with the provided name.  Theorems are put
    1.20 +  into a global ``standard'' format before being stored.
    1.21 +
    1.22 +  \item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a
    1.23 +  singleton theorem.
    1.24    
    1.25    \end{descr}
    1.26  *}

     2.1 --- a/doc-src/IsarRef/style.sty	Thu Nov 13 21:40:00 2008 +0100
     2.2 +++ b/doc-src/IsarRef/style.sty	Thu Nov 13 21:40:30 2008 +0100
     2.3 @@ -16,6 +16,13 @@
     2.4  \newcommand{\figref}[1]{figure~\ref{#1}}
     2.5  \newcommand{\Figref}[1]{Figure~\ref{#1}}
     2.6  
     2.7 +%% index
     2.8 +\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
     2.9 +\newcommand{\indexmlexception}[1]{\index{\emph{#1} (exception)|bold}}
    2.10 +\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
    2.11 +\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
    2.12 +\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
    2.13 +
    2.14  %% math
    2.15  \newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
    2.16  \renewcommand{\isadigit}[1]{\isamath{#1}}