author | wenzelm |
Wed, 06 Dec 2006 01:12:43 +0100 | |
changeset 21672 | 29c346b165d4 |
parent 21671 | f7d652ffef09 |
child 21673 | a664ba87b3aa |
src/HOL/Nat.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Nat.thy Wed Dec 06 01:12:42 2006 +0100 +++ b/src/HOL/Nat.thy Wed Dec 06 01:12:43 2006 +0100 @@ -118,6 +118,13 @@ declare nat.induct [case_names 0 Suc, induct type: nat] declare nat.exhaust [case_names 0 Suc, cases type: nat] +lemmas nat_rec_0 = nat.recs(1) + and nat_rec_Suc = nat.recs(2) + +lemmas nat_case_0 = nat.cases(1) + and nat_case_Suc = nat.cases(2) + + lemma n_not_Suc_n: "n \<noteq> Suc n" by (induct n) simp_all