--- a/ProgTutorial/FirstSteps.thy	Wed Jul 22 08:46:54 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Wed Jul 22 08:54:24 2009 +0200
@@ -472,7 +472,7 @@
   theory and the update also produces a side-result (for example a theorem). Functions 
   for such tasks return a pair whose second component is the theory and the fist 
   component is the side-result. Using @{ML [index] ||>>}, you can do conveniently the update 
-  and also accumulate the side-results. Considder the following simple function. 
+  and also accumulate the side-results. Consider the following simple function. 
 *}
 
 ML %linenosgray{*fun acc_incs x =
@@ -484,7 +484,7 @@
 text {*
   The purpose of Line 2 is to just pair up the argument with a dummy value (since
   @{ML [index] "||>>"} operates on pairs). Each of the next three lines just increment 
-  the value by one, but also nest the intrermediate results to the left. For example 
+  the value by one, but also nest the intermediate results to the left. For example 
 
   @{ML_response [display,gray]
   "acc_incs 1"
@@ -1592,7 +1592,7 @@
   "maintaining a list of my_thms - rough test only!" 
 
 text {*
-  The parser @{ML [index] add_del in Attrib} is a pre-defined parser for 
+  The parser @{ML [index] add_del in Attrib} is a predefined parser for 
   adding and deleting lemmas. Now if you prove the next lemma 
   and attach to it the attribute @{text "[my_thms]"}
 *}
@@ -1660,7 +1660,7 @@
 
 text {*
   where @{ML MyThmsData.map} updates the data appropriately. The
-  corresponding theorem addtributes are
+  corresponding theorem attributes are
 *}
 
 ML{*val my_add = Thm.declaration_attribute my_thm_add
@@ -1900,7 +1900,7 @@
 
 text {*
   So far we printed out only plain strings without any formatting except for
-  occasional explicit linebreaks using @{text [quotes] "\\n"}. This is
+  occasional explicit line breaks using @{text [quotes] "\\n"}. This is
   sufficient for ``quick-and-dirty'' printouts. For something more
   sophisticated, Isabelle includes an infrastructure for properly formatting text.
   This infrastructure is loosely based on a paper by Oppen~\cite{Oppen80}. Most of
@@ -1930,7 +1930,7 @@
 text {*
   The point of the pretty-printing infrastructure is to give hints about how to
   layout text and let Isabelle do the actual layout. Let us first explain
-  how you can insert places where a linebreak can occur. For this assume the
+  how you can insert places where a line break can occur. For this assume the
   following function that replicates a string n times:
 *}
 
@@ -1943,7 +1943,7 @@
 ML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*}
 
 text {*
-  We deliberately chosed a large string so that is spans over more than one line. 
+  We deliberately chose a large string so that is spans over more than one line. 
   If we print out the string using the usual ``quick-and-dirty'' method, then
   we obtain the ugly output:
 
@@ -1964,9 +1964,9 @@
 oooooooooooooobaaaaaaaaaaaar"}
 
   However by using pretty types you have the ability to indicate a possible
-  linebreak for example at each space. You can achieve this with the function
+  line break for example at each space. You can achieve this with the function
   @{ML [index] breaks in Pretty}, which expects a list of pretty types and inserts a
-  possible linebreak in between every two elements in this list. To print
+  possible line break in between every two elements in this list. To print
   this list of pretty types as a single string, we concatenate them 
   with the function @{ML [index] blk in Pretty} as follows:
 
@@ -2048,7 +2048,7 @@
   from the second, each new line as an indentation of 2.
   
   If you print out something that goes beyond the capabilities of the
-  standard functions, you can do realatively easily the formating
+  standard functions, you can do relatively easily the formatting
   yourself. Assume you want to print out a list of items where like in ``English''
   the last two items are separated by @{text [quotes] "and"}. For this you can
   write the function
@@ -2069,8 +2069,8 @@
   where Line 7 prints the beginning of the list and Line
   8 the last item. We have to use @{ML "Pretty.brk 1"} in order
   to insert a space (of length 1) before the 
-  @{text [quotes] "and"}. This space is also a pleace where a linebreak 
-  can occur. We do the same ater the @{text [quotes] "and"}. This gives you
+  @{text [quotes] "and"}. This space is also a place where a line break 
+  can occur. We do the same after the @{text [quotes] "and"}. This gives you
   for example
 
 @{ML_response_fake [display,gray]
@@ -2104,7 +2104,7 @@
   pretty_typ in Syntax}. We also use the function @{ML [index] quote in
   Pretty} in order to enclose the term and type inside quotation marks. In
   Line 9 we add a period right after the type without the possibility of a
-  linebreak, because we do not want that a linebreak occurs there.
+  line break, because we do not want that a line break occurs there.
 
 
   Now you can write
@@ -2113,7 +2113,7 @@
   "tell_type @{context} @{term \"min (Suc 0)\"}"
   "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
   
-  To see the proper linebreaking, you can try out the function on a bigger term 
+  To see the proper line breaking, you can try out the function on a bigger term 
   and type. For example:
 
   @{ML_response_fake [display,gray]