--- a/ProgTutorial/FirstSteps.thy	Thu May 28 12:15:50 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Fri May 29 12:15:48 2009 +0200
@@ -54,20 +54,22 @@
   \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 
+  There are also the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for
+  including ML-code. 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}
+  \begin{quote}
+  \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}
+  \end{quote}
 
-  Inside a proof the \isacommand{ML} will generate an error message.
-  However, both commands will not play any role in this tutorial.
+  However, both commands will not play any role in this tutorial (we, for example, 
+  always assume the ML-code is defined outside proofs).
 
   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 
@@ -99,7 +101,7 @@
   \end{tabular}
   \end{quote}
 
-  Note that no parentheses are given this time.
+  Note that no parentheses are given this time. 
 *}
 
 section {* Debugging and Printing\label{sec:printing} *}
@@ -639,7 +641,7 @@
   representation corresponding to the datatype @{ML_type "term"} defined as follows: 
 *}  
 
-ML_val{*datatype term =
+ML_val %linenosgray{*datatype term =
   Const of string * typ 
 | Free of string * typ 
 | Var of indexname * typ 
@@ -648,8 +650,8 @@
 | $ of term * term *}
 
 text {*
-  Terms use the usual de Bruijn index mechanism---where
-  bound variables are represented by the constructor @{ML Bound}.  For
+  As can be seen in Line 5, terms use the usual de Bruijn index mechanism
+  for representing bound variables.  For
   example in
 
   @{ML_response_fake [display, gray]
@@ -686,12 +688,14 @@
 
   When constructing terms, you are usually concerned with free variables (for example
   you cannot construct schematic variables using the antiquotation @{text "@{term \<dots>}"}). 
-  If you deal with theorems, you have to observe the distinction. A similar
+  If you deal with theorems, you have to, however, observe the distinction. A similar
   distinction holds for types (see below).
 
   \begin{readmore}
   Terms and types are described in detail in \isccite{sec:terms}. Their
   definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
+  For constructing terms involving HOL constants, many helper functions are defined
+  in @{ML_file "HOL/Tools/hologic.ML"}.
   \end{readmore}
   
   Constructing terms via antiquotations has the advantage that only typable

--- a/ProgTutorial/Intro.thy	Thu May 28 12:15:50 2009 +0200
+++ b/ProgTutorial/Intro.thy	Fri May 29 12:15:48 2009 +0200
@@ -10,7 +10,7 @@
   Isabelle programming, and also explain tricks of the trade. The best way to
   get to know the ML-level of Isabelle is by experimenting with the many code
   examples included in the tutorial. The code is as far as possible checked
-  against the Isabelle code.\footnote{\input{version}} If something does not work, 
+  against the Isabelle distribution.\footnote{\input{version}} If something does not work, 
   then please let us know. It is impossible for us to know every environment, 
   operating system or editor in which Isabelle is used. If you have comments, 
   criticism or like to add to the tutorial, please feel free---you are most 
@@ -60,7 +60,7 @@
   things really work. Therefore you should not hesitate to look at the
   way things are actually implemented. More importantly, it is often
   good to look at code that does similar things as you want to do and
-  learn from it. The GNU/UNIX command \mbox{@{text "grep -R"}} is
+  learn from it. The UNIX command \mbox{@{text "grep -R"}} is
   often your best friend while programming with Isabelle, or
   hypersearch if you program using jEdit under MacOSX.
   \end{description}
@@ -122,8 +122,8 @@
 section {* Some Naming Conventions in the Isabelle Sources *}
 
 text {*
-  There are a few naming conventions in Isabelle that might aid reading 
-  and writing code. (Remember that code is written once, but read numerous 
+  There are a few naming conventions in the Isabelle code that might aid reading 
+  and writing code. (Remember that code is written once, but read many 
   times.) The most important conventions are:
 
   \begin{itemize}
@@ -170,7 +170,7 @@
   chapter and also contributed the material on @{text NamedThmsFun}.
 
   \item {\bf Christian Sternagel} proofread the tutorial and made 
-  comments on the text. 
+  many comments on the text. 
   \end{itemize}
 
   Please let me know of any omissions. Responsibility for any remaining

Binary file progtutorial.pdf has changed