# HG changeset patch
# User paulson
# Date 1234259938 0
# Node ID 708c1c7c87ec8930477093d336912cfbc6850b9c
# Parent  55ddff2ed906ecc56a0ed41d586eb2049a1a5e3d# Parent  e2103746a85da9618702877db96afcaa42e07071
merged

diff -r 55ddff2ed906 -r 708c1c7c87ec src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Feb 09 22:15:37 2009 +0100
+++ b/src/HOL/Nat.thy	Tue Feb 10 09:58:58 2009 +0000
@@ -846,13 +846,6 @@
   thus "P i j" by (simp add: j)
 qed
 
-lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n"
-  apply (rule nat_less_induct)
-  apply (case_tac n)
-  apply (case_tac [2] nat)
-  apply (blast intro: less_trans)+
-  done
-
 text {* The method of infinite descent, frequently used in number theory.
 Provided by Roelof Oosterhuis.
 $P(n)$ is true for all $n\in\mathbb{N}$ if
diff -r 55ddff2ed906 -r 708c1c7c87ec src/HOL/ex/Induction_Scheme.thy
--- a/src/HOL/ex/Induction_Scheme.thy	Mon Feb 09 22:15:37 2009 +0100
+++ b/src/HOL/ex/Induction_Scheme.thy	Tue Feb 10 09:58:58 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)