# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1243505750 -7200
# Node ID 3cfd9a8a6de14f5f4fd0a40e98eea196b7e95be1
# Parent  f380b13b25a774e84156feb4551ede85ef1658c6
added comments about ML_prf and ML_val

diff -r f380b13b25a7 -r 3cfd9a8a6de1 ProgTutorial/FirstSteps.thy
--- 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 
diff -r f380b13b25a7 -r 3cfd9a8a6de1 progtutorial.pdf
Binary file progtutorial.pdf has changed