src/HOL/Nat.thy
changeset 29854 708c1c7c87ec
parent 29849 a2baf1b221be
parent 29852 3d4c46f62937
child 29879 4425849f5db7
     1.1 --- a/src/HOL/Nat.thy	Mon Feb 09 22:15:37 2009 +0100
     1.2 +++ b/src/HOL/Nat.thy	Tue Feb 10 09:58:58 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