--- a/Paper/Paper.thy	Wed Oct 06 21:32:44 2010 +0100
+++ b/Paper/Paper.thy	Thu Oct 07 14:23:32 2010 +0900
@@ -1952,7 +1952,7 @@
   \end{array}}
   \end{equation}
   %
-  These cases lemmas have a premise for auch term-constructor.
+  These cases lemmas have a premise for each term-constructor.
   The idea behind them is that we can conclude with a property @{text "P\<^bsub>trm\<^esub>"},
   provided we can show that this property holds if we substitute for @{text "t"} all 
   possible term-constructors. 
@@ -2006,7 +2006,7 @@
   @{text "(set (bn (q \<bullet>\<^bsub>bn\<^esub> p)) \<FRESH>\<^sup>* c"} holds and such that @{text "[q \<bullet>\<^bsub>bn\<^esub> p]\<^bsub>list\<^esub>.(q \<bullet> t)"}
   is equal to @{text "[p]\<^bsub>list\<^esub>. t"}. We can also show that @{text "(q \<bullet>\<^bsub>bn\<^esub> p) \<approx>\<^bsub>bn\<^esub> p"}. But
   these facts establish that @{text "Let (q \<bullet>\<^bsub>bn\<^esub> p) (p \<bullet> t) = Let p t"}, as we need. This
-  completes the interesting cases in \eqref{letpat} for stregthening the induction
+  completes the interesting cases in \eqref{letpat} for strengthening the induction
   principles.