Strengthened the induction rule nat_induct2.
authorpaulson
Tue Feb 10 09:51:23 2009 +0000 (2009-02-10)
changeset 29853e2103746a85d
parent 29852 3d4c46f62937
child 29854 708c1c7c87ec
Strengthened the induction rule nat_induct2.
src/HOL/ex/Induction_Scheme.thy
     1.1 --- a/src/HOL/ex/Induction_Scheme.thy	Tue Feb 10 09:46:11 2009 +0000
     1.2 +++ b/src/HOL/ex/Induction_Scheme.thy	Tue Feb 10 09:51:23 2009 +0000
     1.3 @@ -15,8 +15,8 @@
     1.4    "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P x"
     1.5  by induct_scheme (pat_completeness, lexicographic_order)
     1.6  
     1.7 -lemma nat_induct2: (* cf. Nat.thy *)
     1.8 -  "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc (Suc k)) \<rbrakk>
     1.9 +lemma nat_induct2:
    1.10 +  "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc k) ==> P (Suc (Suc k)) \<rbrakk>
    1.11    \<Longrightarrow> P n"
    1.12  by induct_scheme (pat_completeness, lexicographic_order)
    1.13