--- a/ProgTutorial/FirstSteps.thy	Sat May 30 17:40:20 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Sat May 30 23:58:05 2009 +0200
@@ -318,11 +318,11 @@
 text {* and typographically more economical than *}
 
 ML{*fun inc_by_five x =
-   let val y1 = x + 1
-       val y2 = (y1, y1)
-       val y3 = fst y2
-       val y4 = y3 + 4
-   in y4 end*}
+let val y1 = x + 1
+    val y2 = (y1, y1)
+    val y3 = fst y2
+    val y4 = y3 + 4
+in y4 end*}
 
 text {* 
   Another reason why the let-bindings in the code above are better to be
@@ -339,7 +339,7 @@
       |> map (pair "z")
       |> Variable.variant_frees ctxt [f]
       |> map Free  
-      |> (curry list_comb) f *}
+      |> curry list_comb f *}
 
 text {*
   This code extracts the argument types of a given function @{text "f"} and then generates 
@@ -1966,8 +1966,8 @@
 100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, 
 100016, 100017, 100018, 100019, 100020"}
 
-  where @{ML upto} generates a list of integers. You can print this
-  list out as an ``set'', that means enclosed inside @{text [quotes] "{"} and
+  where @{ML upto} generates a list of integers. You can print out this
+  list as an ``set'', that means enclosed inside @{text [quotes] "{"} and
   @{text [quotes] "}"}, and separated by commas using the function
   @{ML [index] enum in Pretty}. For example
 *}
@@ -1985,10 +1985,10 @@
   100016, 100017, 100018, 100019, 100020}"}
 
   As can be seen, this function prints out the ``set'' so that starting 
-  from the second each new line as an indentation of 2.
+  from the second, each new line as an indentation of 2.
   
-  If you print something out which goes beyond the capabilities of the
-  standard function, you can do realatively easily the formating
+  If you print out something that goes beyond the capabilities of the
+  standard functions, you can do realatively easily the formating
   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
@@ -2006,7 +2006,7 @@
       end *}
 
 text {*
-  where in Line 7 we print the beginning of the list and in Line
+  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 
@@ -2038,14 +2038,15 @@
 end*}
 
 text {*
-  In Line 3 we define a function that inserts according to spaces 
-  possible linebreaks into an (English). In Lines 4 and 5 we pretty-print
-  the term and its type using the functions @{ML [index] pretty_term in Syntax} and
-  @{ML [index] 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 
+  In Line 3 we define a function that inserts possible linebreaks in places
+  where a space is. In Lines 4 and 5 we pretty-print the term and its type
+  using the functions @{ML [index] pretty_term in Syntax} and @{ML [index]
+  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.
 
+
   Now you can write
 
   @{ML_response_fake [display,gray]
@@ -2060,6 +2061,8 @@
   "The term \"op = (op = (op = (op = (op = op =))))\" has type 
 \"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
 
+
+  FIXME: TBD below
 *}
 
 ML {* pprint (Pretty.big_list "header"  (map (Pretty.str o string_of_int) (4 upto 10))) *}