# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1237829321 -3600
# Node ID abdac57dfd9a48468da29110ea96f118269aab0b
# Parent  8cd51a25a7caaa6b40c4d67e2d190675be1df623# Parent  7305beb698939f86d5ecab72959d898aa1f6afb6
merged

diff -r 8cd51a25a7ca -r abdac57dfd9a ProgTutorial/Intro.thy
--- 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
diff -r 8cd51a25a7ca -r abdac57dfd9a progtutorial.pdf