added aliases for nat_recs/cases;
authorwenzelm
Wed, 06 Dec 2006 01:12:43 +0100
changeset 21672 29c346b165d4
parent 21671 f7d652ffef09
child 21673 a664ba87b3aa
added aliases for nat_recs/cases;
src/HOL/Nat.thy
--- 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