--- a/Tutorial/Tutorial1.thy	Sun Jan 23 07:15:59 2011 +0900
+++ b/Tutorial/Tutorial1.thy	Tue Jan 25 02:46:05 2011 +0900
@@ -132,7 +132,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
@@ -395,14 +395,14 @@
   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.
 *}
  
 
 
 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	Sun Jan 23 07:15:59 2011 +0900
+++ b/Tutorial/Tutorial4.thy	Tue Jan 25 02:46:05 2011 +0900
@@ -6,8 +6,8 @@
 section {* The CBV Reduction Relation (Small-Step Semantics) *}
 
 text {*
-  In order to help establishing the property that the CK Machine
-  calculates a nomrmalform that corresponds to the evaluation 
+  In order to help establishing the property that the Machine
+  calculates a normal form that corresponds to the evaluation 
   relation, we introduce the call-by-value small-step semantics.
 *}
 
@@ -106,7 +106,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: