doc-src/IsarRef/Thy/Spec.thy
changeset 30461 00323c45ea83
parent 30242 aea5d7fa7ef5
child 30526 7f9a9ec1c94d
     1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Wed Mar 11 20:54:03 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Mar 11 23:59:34 2009 +0100
     1.3 @@ -799,6 +799,7 @@
     1.4      @{command_def "ML_val"} & : & @{text "any \<rightarrow>"} \\
     1.5      @{command_def "ML_command"} & : & @{text "any \<rightarrow>"} \\
     1.6      @{command_def "setup"} & : & @{text "theory \<rightarrow> theory"} \\
     1.7 +    @{command_def "local_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     1.8    \end{matharray}
     1.9  
    1.10    \begin{mldecls}
    1.11 @@ -809,7 +810,7 @@
    1.12    \begin{rail}
    1.13      'use' name
    1.14      ;
    1.15 -    ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup') text
    1.16 +    ('ML' | 'ML\_prf' | 'ML\_val' | 'ML\_command' | 'setup' | 'local\_setup') text
    1.17      ;
    1.18    \end{rail}
    1.19  
    1.20 @@ -817,7 +818,7 @@
    1.21  
    1.22    \item @{command "use"}~@{text "file"} reads and executes ML
    1.23    commands from @{text "file"}.  The current theory context is passed
    1.24 -  down to the ML toplevel and may be modified, using @{ML [source=false]
    1.25 +  down to the ML toplevel and may be modified, using @{ML
    1.26    "Context.>>"} or derived ML commands.  The file name is checked with
    1.27    the @{keyword_ref "uses"} dependency declaration given in the theory
    1.28    header (see also \secref{sec:begin-thy}).
    1.29 @@ -845,9 +846,15 @@
    1.30    
    1.31    \item @{command "setup"}~@{text "text"} changes the current theory
    1.32    context by applying @{text "text"}, which refers to an ML expression
    1.33 -  of type @{ML_type [source=false] "theory -> theory"}.  This enables
    1.34 -  to initialize any object-logic specific tools and packages written
    1.35 -  in ML, for example.
    1.36 +  of type @{ML_type "theory -> theory"}.  This enables to initialize
    1.37 +  any object-logic specific tools and packages written in ML, for
    1.38 +  example.
    1.39 +
    1.40 +  \item @{command "local_setup"} is similar to @{command "setup"} for
    1.41 +  a local theory context, and an ML expression of type @{ML_type
    1.42 +  "local_theory -> local_theory"}.  This allows to
    1.43 +  invoke local theory specification packages without going through
    1.44 +  concrete outer syntax, for example.
    1.45  
    1.46    \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
    1.47    theorems produced in ML both in the theory context and the ML