Deleted the induction rule nat_induct2, which was too weak and not used even once.

1.1 --- a/src/HOL/Nat.thy Mon Feb 09 11:15:13 2009 +0000
1.2 +++ b/src/HOL/Nat.thy Tue Feb 10 09:46:11 2009 +0000
1.3 @@ -846,13 +846,6 @@
1.4 thus "P i j" by (simp add: j)
1.5 qed
1.6
1.7 -lemma nat_induct2: "[|P 0; P (Suc 0); !!k. P k ==> P (Suc (Suc k))|] ==> P n"
1.8 - apply (rule nat_less_induct)
1.9 - apply (case_tac n)
1.10 - apply (case_tac [2] nat)
1.11 - apply (blast intro: less_trans)+
1.12 - done
1.13 -
1.14 text {* The method of infinite descent, frequently used in number theory.
1.15 Provided by Roelof Oosterhuis.
1.16 $P(n)$ is true for all $n\in\mathbb{N}$ if