# HG changeset patch # User wenzelm # Date 1345668436 -7200 # Node ID d72ca5742f80e27eefffe76ae6bed08afd042b4f # Parent 04deeb14327c78556764bef5e0ee4c4e7b7c71d0 'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses'; diff -r 04deeb14327c -r d72ca5742f80 NEWS --- a/NEWS Wed Aug 22 21:43:17 2012 +0200 +++ b/NEWS Wed Aug 22 22:47:16 2012 +0200 @@ -6,6 +6,9 @@ *** General *** +* Command 'ML_file' evaluates ML text from a file directly within the +theory, without any predeclaration via 'uses' in the theory header. + * Discontinued obsolete method fastsimp / tactic fast_simp_tac, which is called fastforce / fast_force_tac already since Isabelle2011-1. diff -r 04deeb14327c -r d72ca5742f80 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Wed Aug 22 21:43:17 2012 +0200 +++ b/doc-src/IsarRef/Thy/Spec.thy Wed Aug 22 22:47:16 2012 +0200 @@ -960,7 +960,7 @@ text {* \begin{matharray}{rcl} - @{command_def "use"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "ML_file"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "ML"} & : & @{text "local_theory \ local_theory"} \\ @{command_def "ML_prf"} & : & @{text "proof \ proof"} \\ @{command_def "ML_val"} & : & @{text "any \"} \\ @@ -971,7 +971,7 @@ \end{matharray} @{rail " - @@{command use} @{syntax name} + @@{command ML_file} @{syntax name} ; (@@{command ML} | @@{command ML_prf} | @@{command ML_val} | @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text} @@ -981,28 +981,22 @@ \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 - "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 - context. + \item @{command "ML_file"}~@{text "name"} reads and evaluates the + given ML file. The current theory context is passed down to the ML + toplevel and may be modified, using @{ML "Context.>>"} or derived ML + commands. Top-level ML bindings are stored within the (global or + local) theory context. - \item @{command "ML"}~@{text "text"} is similar to @{command "use"}, - but executes ML commands directly from the given @{text "text"}. + \item @{command "ML"}~@{text "text"} is similar to @{command + "ML_file"}, but evaluates directly the given @{text "text"}. Top-level ML bindings are stored within the (global or local) theory context. \item @{command "ML_prf"} is analogous to @{command "ML"} but works - within a proof context. - - Top-level ML bindings are stored within the proof context in a - purely sequential fashion, disregarding the nested proof structure. - ML bindings introduced by @{command "ML_prf"} are discarded at the - end of the proof. + within a proof context. Top-level ML bindings are stored within the + proof context in a purely sequential fashion, disregarding the + nested proof structure. ML bindings introduced by @{command + "ML_prf"} are discarded at the end of the proof. \item @{command "ML_val"} and @{command "ML_command"} are diagnostic versions of @{command "ML"}, which means that the context may not be diff -r 04deeb14327c -r d72ca5742f80 doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Wed Aug 22 21:43:17 2012 +0200 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Wed Aug 22 22:47:16 2012 +0200 @@ -1444,7 +1444,7 @@ % \begin{isamarkuptext}% \begin{matharray}{rcl} - \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ + \indexdef{}{command}{ML\_file}\hypertarget{command.ML-file}{\hyperlink{command.ML-file}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}file}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{ML\_prf}\hypertarget{command.ML-prf}{\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ @@ -1456,7 +1456,7 @@ \begin{railoutput} \rail@begin{1}{} -\rail@term{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}}[] +\rail@term{\hyperlink{command.ML-file}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}file}}}}}[] \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] \rail@end \rail@begin{6}{} @@ -1490,27 +1490,20 @@ \begin{description} - \item \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}} reads and executes ML - commands from \isa{{\isaliteral{22}{\isachardoublequote}}file{\isaliteral{22}{\isachardoublequote}}}. The current theory context is passed - down to the ML toplevel and may be modified, using \verb|Context.>>| or derived ML commands. The file name is checked with - the \indexref{}{keyword}{uses}\hyperlink{keyword.uses}{\mbox{\isa{\isakeyword{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 - context. + \item \hyperlink{command.ML-file}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}file}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{22}{\isachardoublequote}}} reads and evaluates the + given ML file. The current theory context is passed down to the ML + toplevel and may be modified, using \verb|Context.>>| or derived ML + commands. Top-level ML bindings are stored within the (global or + local) theory context. - \item \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}, - but executes ML commands directly from the given \isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}}. + \item \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}} is similar to \hyperlink{command.ML-file}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}file}}}}, but evaluates directly the given \isa{{\isaliteral{22}{\isachardoublequote}}text{\isaliteral{22}{\isachardoublequote}}}. Top-level ML bindings are stored within the (global or local) theory context. \item \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}} is analogous to \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} but works - within a proof context. - - Top-level ML bindings are stored within the proof context in a - purely sequential fashion, disregarding the nested proof structure. - ML bindings introduced by \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}} are discarded at the - end of the proof. + within a proof context. Top-level ML bindings are stored within the + proof context in a purely sequential fashion, disregarding the + nested proof structure. ML bindings introduced by \hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}prf}}}} are discarded at the end of the proof. \item \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isaliteral{5F}{\isacharunderscore}}command}}}} are diagnostic versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context may not be