Deleted the induction rule nat_induct2, which was too weak and not used even once.
authorpaulson
Tue Feb 10 09:46:11 2009 +0000 (2009-02-10)
changeset 298523d4c46f62937
parent 29836 3d935e8b0bf7
child 29853 e2103746a85d
Deleted the induction rule nat_induct2, which was too weak and not used even once.
src/HOL/Nat.thy
     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