doc-src/IsarRef/Thy/document/Spec.tex
changeset 30463 f1cb00030d4f
parent 30242 aea5d7fa7ef5
child 30527 fae488569faf
     1.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Thu Mar 12 00:02:03 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Thu Mar 12 00:02:30 2009 +0100
     1.3 @@ -807,6 +807,7 @@
     1.4      \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
     1.5      \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
     1.6      \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     1.7 +    \indexdef{}{command}{local\_setup}\hypertarget{command.local-setup}{\hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
     1.8    \end{matharray}
     1.9  
    1.10    \begin{mldecls}
    1.11 @@ -817,7 +818,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 @@ -852,9 +853,14 @@
    1.21    
    1.22    \item \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}} changes the current theory
    1.23    context by applying \isa{{\isachardoublequote}text{\isachardoublequote}}, which refers to an ML expression
    1.24 -  of type \verb|theory -> theory|.  This enables
    1.25 -  to initialize any object-logic specific tools and packages written
    1.26 -  in ML, for example.
    1.27 +  of type \verb|theory -> theory|.  This enables to initialize
    1.28 +  any object-logic specific tools and packages written in ML, for
    1.29 +  example.
    1.30 +
    1.31 +  \item \hyperlink{command.local-setup}{\mbox{\isa{\isacommand{local{\isacharunderscore}setup}}}} is similar to \hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}} for
    1.32 +  a local theory context, and an ML expression of type \verb|local_theory -> local_theory|.  This allows to
    1.33 +  invoke local theory specification packages without going through
    1.34 +  concrete outer syntax, for example.
    1.35  
    1.36    \item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of
    1.37    theorems produced in ML both in the theory context and the ML