src/Doc/IsarRef/Spec.thy
changeset 56275 600f432ab556
parent 55837 154855d9a564
     1.1 --- a/src/Doc/IsarRef/Spec.thy	Tue Mar 25 10:37:10 2014 +0100
     1.2 +++ b/src/Doc/IsarRef/Spec.thy	Tue Mar 25 13:18:10 2014 +0100
     1.3 @@ -1000,6 +1000,7 @@
     1.4  
     1.5  text {*
     1.6    \begin{matharray}{rcl}
     1.7 +    @{command_def "SML_file"} & : & @{text "theory \<rightarrow> theory"} \\
     1.8      @{command_def "ML_file"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     1.9      @{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    1.10      @{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\
    1.11 @@ -1011,7 +1012,7 @@
    1.12    \end{matharray}
    1.13  
    1.14    @{rail \<open>
    1.15 -    @@{command ML_file} @{syntax name}
    1.16 +    (@@{command SML_file} | @@{command ML_file}) @{syntax name}
    1.17      ;
    1.18      (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
    1.19        @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
    1.20 @@ -1021,6 +1022,14 @@
    1.21  
    1.22    \begin{description}
    1.23  
    1.24 +  \item @{command "SML_file"}~@{text "name"} reads and evaluates the
    1.25 +  given Standard ML file.  Top-level SML bindings are stored within
    1.26 +  the theory context; the initial environment is restricted to the
    1.27 +  Standard ML implementation of Poly/ML, without the many add-ons of
    1.28 +  Isabelle/ML.  Multiple @{command "SML_file"} commands may be used to
    1.29 +  build larger Standard ML projects, independently of the regular
    1.30 +  Isabelle/ML environment.
    1.31 +
    1.32    \item @{command "ML_file"}~@{text "name"} reads and evaluates the
    1.33    given ML file.  The current theory context is passed down to the ML
    1.34    toplevel and may be modified, using @{ML "Context.>>"} or derived ML