--- a/ProgTutorial/FirstSteps.thy	Mon Mar 23 12:35:15 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Mon Mar 23 12:47:05 2009 +0100
@@ -541,7 +541,7 @@
   (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 
   will show the term @{term "(a::nat) + b = c"}, but printed using an internal
-  representation corresponding to the datatype @{ML_type "term"}.
+  representation corresponding to the data type @{ML_type "term"}.
   
   This internal representation uses the usual de Bruijn index mechanism---where
   bound variables are represented by the constructor @{ML Bound}.  The index in
@@ -750,7 +750,7 @@
   @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
 
   the name of the constant @{text "Nil"} depends on the theory in which the
-  term constructor is defined (@{text "List"}) and also in which datatype
+  term constructor is defined (@{text "List"}) and also in which data type
   (@{text "list"}). Even worse, some constants have a name involving
   type-classes. Consider for example the constants for @{term "zero"} and
   \mbox{@{text "(op *)"}}:
@@ -762,7 +762,7 @@
   While you could use the complete name, for example 
   @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
   matching against @{text "Nil"}, this would make the code rather brittle. 
-  The reason is that the theory and the name of the datatype can easily change. 
+  The reason is that the theory and the name of the data type can easily change. 
   To make the code more robust, it is better to use the antiquotation 
   @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the 
   variable parts of the constant's name. Therefore a functions for 
@@ -868,7 +868,7 @@
 end" "0 + 0"}
 
   In Isabelle not just terms need to be certified, but also types. For example, 
-  you obtain the certified type for the Isablle type @{typ "nat \<Rightarrow> bool"} on 
+  you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on 
   the ML-level as follows:
 
   @{ML_response_fake [display,gray]