doc-src/IsarRef/Thy/Spec.thy

     @{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
     @{command_def "ML_prf"} & : & \isarkeep{proof} \\
     @{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}
     'use' name
     ;

   \item [@{command "setup"}~@{text "text"}] changes the current theory
   context by applying @{text "text"}, which refers to an ML expression
   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}
 *}