# HG changeset patch
# User paulson
# Date 1234259483 0
# Node ID e2103746a85da9618702877db96afcaa42e07071
# Parent  3d4c46f62937c8a89891bf012389541a31ac8416
Strengthened the induction rule nat_induct2.

diff -r 3d4c46f62937 -r e2103746a85d src/HOL/ex/Induction_Scheme.thy
--- a/src/HOL/ex/Induction_Scheme.thy	Tue Feb 10 09:46:11 2009 +0000
+++ b/src/HOL/ex/Induction_Scheme.thy	Tue Feb 10 09:51:23 2009 +0000
@@ -15,8 +15,8 @@
   "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P x"
 by induct_scheme (pat_completeness, lexicographic_order)
 
-lemma nat_induct2: (* cf. Nat.thy *)
-  "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc (Suc k)) \<rbrakk>
+lemma nat_induct2:
+  "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc k) ==> P (Suc (Suc k)) \<rbrakk>
   \<Longrightarrow> P n"
 by induct_scheme (pat_completeness, lexicographic_order)