# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266418328 -3600
# Node ID 789fbba5c23fc84767d61d49d0722d739fb2b629
# Parent  275a1cb3f2bac1888bb891ee0b10a17689ba8b54
Fix the strong induction principle.

diff -r 275a1cb3f2ba -r 789fbba5c23f Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 17 15:45:03 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 17 15:52:08 2010 +0100
@@ -271,7 +271,7 @@
   assumes "\<And>name b. P b (Vr1 name)"
   and     "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"
   and     "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"
-  and     "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bp1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
+  and     "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bv1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"
   shows   "P a rtrma"
 sorry