--- a/ProgTutorial/FirstSteps.thy	Sat May 23 02:19:54 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Thu May 28 12:15:50 2009 +0200
@@ -54,6 +54,20 @@
   \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we
   show code. The lines prefixed with @{text [quotes] ">"} are not part of the
   code, rather they indicate what the response is when the code is evaluated.
+  There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf}.
+  The first evaluates the given code, but any effect on the ambient
+  theory is suppressed. The second needs to be used if ML-code is defined 
+  inside a proof. For example
+
+\begin{isabelle}
+\isacommand{lemma}~@{text "test:"}\isanewline
+\isacommand{shows}~@{text [quotes] "True"}\isanewline
+\isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial\""}~@{text "\<verbclose>"}\isanewline
+\isacommand{oops}
+\end{isabelle}
+
+  Inside a proof the \isacommand{ML} will generate an error message.
+  However, both commands will not play any role in this tutorial.
 
   Once a portion of code is relatively stable, you usually want to export it
   to a separate ML-file. Such files can then be included somewhere inside a