--- a/Tutorial/Tutorial1.thy	Wed Feb 29 17:14:31 2012 +0000
+++ b/Tutorial/Tutorial1.thy	Mon Mar 05 16:27:28 2012 +0000
@@ -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 overloaded function *}
+term "atom (x::name)"  -- {* atom is an overloded function *}
 
 text {* 
   Lam [x].Var is the syntax we made up for lambda abstractions. If you
@@ -207,7 +207,7 @@
 *}
 
 inductive
-  eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infixr "\<Down>" 60)
+  eval :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<Down> _" [60, 60] 60) 
 where
   e_Lam[intro]:  "Lam [x].t \<Down> Lam [x].t"
 | e_App[intro]:  "\<lbrakk>t1 \<Down> Lam [x].t; t2 \<Down> v'; t[x::=v'] \<Down> v\<rbrakk> \<Longrightarrow> App t1 t2 \<Down> v"
@@ -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 the second case below.
+  the next have-statement. This is used in teh 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 rearrange them. We can still avoid the
+  two lines below and we cannot rearange them. We can still avoid the
   label by feeding a sequence of facts into a proof using the 
   "moreover"-chaining mechanism: