--- a/ProgTutorial/Essential.thy	Sun Oct 30 17:45:10 2011 +0000
+++ b/ProgTutorial/Essential.thy	Wed Nov 02 13:38:19 2011 +0000
@@ -263,8 +263,7 @@
   we can see the full name of the type is actually @{text "List.list"}, indicating
   that it is defined in the theory @{text "List"}. However, one has to be 
   careful with names of types, because even if
-  @{text "fun"}, @{text "bool"} and @{text "nat"} are defined in the 
-  theories @{text "HOL"} and @{text "Nat"}, respectively, they are 
+  @{text "fun"} is defined in the theory @{text "HOL"}, it is  
   still represented by their simple name.
 
    @{ML_response [display,gray]
@@ -384,7 +383,7 @@
 end"
   "Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}
 
-  then the variable @{text "Free (\"x\", \"int\")"} is \emph{not} abstracted. 
+  then the variable @{text "Free (\"x\", \"nat\")"} is \emph{not} abstracted. 
   This is a fundamental principle
   of Church-style typing, where variables with the same name still differ, if they 
   have different type.

--- a/ProgTutorial/First_Steps.thy	Sun Oct 30 17:45:10 2011 +0000
+++ b/ProgTutorial/First_Steps.thy	Wed Nov 02 13:38:19 2011 +0000
@@ -508,9 +508,10 @@
 
 text {*
   The function @{ML_text "my_note"} in line 3 is just a wrapper for the function 
-  @{ML_ind note in Local_Theory}; its purpose is to store a theorem under a name. 
-  In lines 5 to 6 we call this function to give alternative names for three
-  theorems. The point of @{ML "#>"} is that you can sequence such functions. 
+  @{ML_ind note in Local_Theory} in the structure @{ML_struct Local_Theory}; 
+  its purpose is to store a theorem under a name. 
+  In lines 5 to 6 we call this function to give alternative names for the three
+  theorems. The point of @{ML "#>"} is that you can sequence such function calls. 
 
   The remaining combinators we describe in this section add convenience for
   the ``waterfall method'' of writing functions. The combinator @{ML_ind tap

Binary file progtutorial.pdf has changed