# HG changeset patch
# User wenzelm
# Date 1221685686 -7200
# Node ID 132456af0731c7a37404caea5c2811c1473bf7b4
# Parent  fd0485db7d5a2a7ef37b191fdffc45252ab1a86e
added ML_prf;

diff -r fd0485db7d5a -r 132456af0731 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Wed Sep 17 23:04:27 2008 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Sep 17 23:08:06 2008 +0200
@@ -802,6 +802,7 @@
   \begin{matharray}{rcl}
     @{command_def "use"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
     @{command_def "ML"} & : & \isarkeep{theory~|~local{\dsh}theory} \\
+    @{command_def "ML_prf"} & : & \isarkeep{proof} \\
     @{command_def "ML_val"} & : & \isartrans{\cdot}{\cdot} \\
     @{command_def "ML_command"} & : & \isartrans{\cdot}{\cdot} \\
     @{command_def "setup"} & : & \isartrans{theory}{theory} \\
@@ -825,10 +826,22 @@
   "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"}~@{text "text"}] is similar to @{command
   "use"}, but executes ML commands directly from the given @{text
-  "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.
 
   \item [@{command "ML_val"} and @{command "ML_command"}] are
   diagnostic versions of @{command "ML"}, which means that the context
diff -r fd0485db7d5a -r 132456af0731 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Wed Sep 17 23:04:27 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Wed Sep 17 23:08:06 2008 +0200
@@ -806,6 +806,7 @@
 \begin{matharray}{rcl}
     \indexdef{}{command}{use}\hypertarget{command.use}{\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
     \indexdef{}{command}{ML}\hypertarget{command.ML}{\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}} & : & \isarkeep{theory~|~local{\dsh}theory} \\
+    \indexdef{}{command}{ML\_prf}\hypertarget{command.ML-prf}{\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}}} & : & \isarkeep{proof} \\
     \indexdef{}{command}{ML\_val}\hypertarget{command.ML-val}{\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}}} & : & \isartrans{\cdot}{\cdot} \\
     \indexdef{}{command}{ML\_command}\hypertarget{command.ML-command}{\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}} & : & \isartrans{\cdot}{\cdot} \\
     \indexdef{}{command}{setup}\hypertarget{command.setup}{\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}}} & : & \isartrans{theory}{theory} \\
@@ -828,8 +829,20 @@
   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}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}, but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.
+  \item [\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] is similar to \hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}}, but executes ML commands directly from the given \isa{{\isachardoublequote}text{\isachardoublequote}}.  Top-level ML bindings are stored within the (global or
+  local) theory context.
+
+  \item [\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\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{\isacharunderscore}prf}}}} are discarded at the
+  end of the proof.
 
   \item [\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}}] are
   diagnostic versions of \hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which means that the context