--- a/Tutorial/Tutorial4.thy	Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Tutorial4.thy	Mon Mar 05 16:27:28 2012 +0000
@@ -49,7 +49,7 @@
 
 text {*
   In order to help establishing the property that the machine
-  calculates a normal form that corresponds to the evaluation 
+  calculates a nomrmalform 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 following property:
+  establish the follwoing property:
 *}
 
 lemma machine_implies_cbvs_ctx: