merged
authorpaulson
Tue Feb 10 09:58:58 2009 +0000 (2009-02-10)
changeset 29854708c1c7c87ec
parent 29851 55ddff2ed906
parent 29853 e2103746a85d
child 29855 e0ab6cf95539
merged
src/HOL/Nat.thy
     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
     2.1 --- a/src/HOL/ex/Induction_Scheme.thy	Mon Feb 09 22:15:37 2009 +0100
     2.2 +++ b/src/HOL/ex/Induction_Scheme.thy	Tue Feb 10 09:58:58 2009 +0000
     2.3 @@ -15,8 +15,8 @@
     2.4    "\<lbrakk>P 0; \<And>n. P n \<Longrightarrow> P (Suc n)\<rbrakk> \<Longrightarrow> P x"
     2.5  by induct_scheme (pat_completeness, lexicographic_order)
     2.6  
     2.7 -lemma nat_induct2: (* cf. Nat.thy *)
     2.8 -  "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc (Suc k)) \<rbrakk>
     2.9 +lemma nat_induct2:
    2.10 +  "\<lbrakk> P 0; P (Suc 0); \<And>k. P k ==> P (Suc k) ==> P (Suc (Suc k)) \<rbrakk>
    2.11    \<Longrightarrow> P n"
    2.12  by induct_scheme (pat_completeness, lexicographic_order)
    2.13