--- 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: