--- a/Tutorial/Tutorial1.thy	Tue Jan 25 02:42:15 2011 +0900
+++ b/Tutorial/Tutorial1.thy	Tue Jan 25 02:51:44 2011 +0900
@@ -131,7 +131,7 @@
 term "Lam [x].Var x"   -- {* a lambda-term *}
 term "App t1 t2"       -- {* another lambda-term *}
 term "x::name"         -- {* an (object) variable of type name *}
-term "atom (x::name)"  -- {* atom is an overloded function *}
+term "atom (x::name)"  -- {* atom is an overloaded function *}
 
 text {* 
   Lam [x].Var is the syntax we made up for lambda abstractions. If you
@@ -476,7 +476,7 @@
   Just like gotos in the Basic programming language, labels often reduce 
   the readability of proofs. Therefore one can use in Isar the notation
   "then have" in order to feed a have-statement to the proof of 
-  the next have-statement. This is used in teh second case below.
+  the next have-statement. This is used in the second case below.
 *}
  
 lemma 
@@ -498,7 +498,7 @@
 
 text {* 
   The label ih2 cannot be got rid of in this way, because it is used 
-  two lines below and we cannot rearange them. We can still avoid the
+  two lines below and we cannot rearrange them. We can still avoid the
   label by feeding a sequence of facts into a proof using the 
   "moreover"-chaining mechanism:
 

--- a/Tutorial/Tutorial4.thy	Tue Jan 25 02:42:15 2011 +0900
+++ b/Tutorial/Tutorial4.thy	Tue Jan 25 02:51:44 2011 +0900
@@ -49,7 +49,7 @@
 
 text {*
   In order to help establishing the property that the machine
-  calculates a nomrmalform that corresponds to the evaluation 
+  calculates a normal form that corresponds to the evaluation 
   relation, we introduce the call-by-value small-step semantics.
 *}
 
@@ -124,7 +124,7 @@
  
 text {*
   The point of the cbv-reduction was that we can easily relatively 
-  establish the follwoing property:
+  establish the following property:
 *}
 
 lemma machine_implies_cbvs_ctx: