doc-src/IsarRef/Thy/Spec.thy

     @{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\
     @{command_def "ML_val"} & : & @{text "any \<rightarrow>"} \\
     @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
     @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_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
     ;
-    ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup') text
+    ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
     ;
   \end{rail}
 
   \begin{description}
 
   \item @{command "use"}~@{text "file"} reads and executes ML
   commands from @{text "file"}.  The current theory context is passed
-  down to the ML toplevel and may be modified, using @{ML [source=false]
+  down to the ML toplevel and may be modified, using @{ML
   "Context.>>"} or derived ML commands.  The file name is checked with
   the @{keyword_ref "uses"} dependency declaration given in the theory
   header (see also \secref{sec:begin-thy}).
 
   Top-level ML bindings are stored within the (global or local) theory

   updated.  @{command "ML_val"} echos the bindings produced at the ML
   toplevel, but @{command "ML_command"} is silent.
   
   \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.
+  of type @{ML_type "theory -> theory"}.  This enables to initialize
+  any object-logic specific tools and packages written in ML, for
+  example.
+
+  \item @{command "local_setup"} is similar to @{command "setup"} for
+  a local theory context, and an ML expression of type @{ML_type
+  "local_theory -> local_theory"}.  This allows to
+  invoke local theory specification packages without going through
+  concrete outer syntax, 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.