--- a/ProgTutorial/Intro.thy	Mon Mar 23 18:17:24 2009 +0100
+++ b/ProgTutorial/Intro.thy	Mon Mar 23 18:28:41 2009 +0100
@@ -56,11 +56,11 @@
   Then of course there is:
 
   \begin{description}
-  \item[The code] is of course the ultimate reference for how
+  \item[The code.] Which is the ultimate reference for how
   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
-  to learn from that code. The UNIX command @{text "grep -R"} is
+  learn from it. The UNIX command @{text "grep -R"} is
   often your best friend while programming with Isabelle. 
   \end{description}
 
@@ -81,7 +81,7 @@
   \end{graybox}
   \end{isabelle}
   
-  These boxes corresponds to how code can be processed inside the interactive
+  These boxes correspond to how code can be processed inside the interactive
   environment of Isabelle. It is therefore easy to experiment with what is 
   displayed. However, for better readability we will drop the enclosing 
   \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write:
@@ -95,15 +95,15 @@
 
   @{ML_response [display,gray] "3 + 4" "7"}
 
-  The user-level commands of Isabelle (i.e.~the non-ML code) are written
-  in bold, for example \isacommand{lemma}, \isacommand{apply},
-  \isacommand{foobar} and so on.  We use @{text "$ \<dots>"} to indicate that a
+  The user-level commands of Isabelle (i.e., the non-ML code) are written
+  in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},
+  \isacommand{foobar} and so on).  We use @{text "$ \<dots>"} to indicate that a
   command needs to be run in a Unix-shell, for example:
 
   @{text [display] "$ grep -R ThyOutput *"}
 
   Pointers to further information and Isabelle files are typeset in 
-  italic and highlighted as follows:
+  \textit{italic} and highlighted as follows:
 
   \begin{readmore}
   Further information or pointers to files.
@@ -166,4 +166,4 @@
 
 
 
-end
\ No newline at end of file
+end