# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1286429012 -32400
# Node ID 06a8f782b2c14026409fee699eddac0bd6c308f0
# Parent  69780ae147f58193aedd8f840b6b3b84fb321ecb
minor

diff -r 69780ae147f5 -r 06a8f782b2c1 Paper/Paper.thy
--- 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.