--- a/doc-src/IsarRef/pure.tex Tue Mar 25 21:28:39 2008 +0100
+++ b/doc-src/IsarRef/pure.tex Tue Mar 25 21:47:19 2008 +0100
@@ -466,35 +466,28 @@
\subsection{Incorporating ML code}\label{sec:ML}
-\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-command}
+\indexisarcmd{use}\indexisarcmd{ML}
+\indexisarcmd{ML-val}\indexisarcmd{ML-command}
\indexisarcmd{ML-setup}\indexisarcmd{setup}
\indexisarcmd{method-setup}
\begin{matharray}{rcl}
\isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
\isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
+ \isarcmd{ML_val} & : & \isartrans{\cdot}{\cdot} \\
\isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\
\isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
\isarcmd{setup} & : & \isartrans{theory}{theory} \\
\isarcmd{method_setup} & : & \isartrans{theory}{theory} \\
\end{matharray}
-\railalias{MLsetup}{ML\_setup}
-\railterm{MLsetup}
-
-\railalias{methodsetup}{method\_setup}
-\railterm{methodsetup}
-
-\railalias{MLcommand}{ML\_command}
-\railterm{MLcommand}
-
\begin{rail}
'use' name
;
- ('ML' | MLcommand | MLsetup) text
+ ('ML' | 'ML\_val' | 'ML\_command' | 'ML\_setup') text
;
'setup' text?
;
- methodsetup name '=' text text
+ 'method\_setup' name '=' text text
;
\end{rail}
@@ -505,10 +498,12 @@
$\isarkeyword{files}$ dependency declaration given in the theory header (see
also \S\ref{sec:begin-thy}).
-\item [$\isarkeyword{ML}~text$ and $\isarkeyword{ML_command}~text$] execute ML
- commands from $text$. The theory context is passed in the same way as for
- $\isarkeyword{use}$, but may not be changed. Note that the output of
- $\isarkeyword{ML_command}$ is less verbose than plain $\isarkeyword{ML}$.
+\item [$\isarkeyword{ML}~text$ and $\isarkeyword{ML_val}~text$ and
+ $\isarkeyword{ML_command}~text$] execute ML commands from $text$.
+ The theory context is passed in the same way as for
+ $\isarkeyword{use}$, but may not be changed. Note that the output
+ of $\isarkeyword{ML_command}$ is less verbose than plain
+ $\isarkeyword{ML}$.
\item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$. The
theory context is passed down to the ML session, and fetched back