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