Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Strengthened the induction rule nat_induct2.
authorpaulson
Tue, 10 Feb 2009 09:51:23 +0000
changeset 29853 e2103746a85d
parent 29852 3d4c46f62937
child 29854 708c1c7c87ec
Strengthened the induction rule nat_induct2.
src/HOL/ex/Induction_Scheme.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/ex/Induction_Scheme.thy	Tue Feb 10 09:46:11 2009 +0000
+++ b/src/HOL/ex/Induction_Scheme.thy	Tue Feb 10 09:51:23 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)
isabelle