src/HOL/Nat.thy
 changeset 55415 05f5fdb8d093 parent 54742 7a86358a3c0b child 55417 01fbfb60c33e
```     1.1 --- a/src/HOL/Nat.thy	Wed Feb 12 08:35:57 2014 +0100
1.2 +++ b/src/HOL/Nat.thy	Wed Feb 12 08:35:57 2014 +0100
1.3 @@ -95,8 +95,8 @@
1.4  lemmas nat_rec_0 = nat.recs(1)
1.5    and nat_rec_Suc = nat.recs(2)
1.6
1.7 -lemmas nat_case_0 = nat.cases(1)
1.8 -  and nat_case_Suc = nat.cases(2)
1.9 +lemmas case_nat_0 = nat.cases(1)
1.10 +  and case_nat_Suc = nat.cases(2)
1.11
1.12
1.13  text {* Injectiveness and distinctness lemmas *}
1.14 @@ -634,10 +634,10 @@
1.15
1.16  text {* These two rules ease the use of primitive recursion.
1.17  NOTE USE OF @{text "=="} *}
1.18 -lemma def_nat_rec_0: "(!!n. f n == nat_rec c h n) ==> f 0 = c"
1.19 +lemma def_rec_nat_0: "(!!n. f n == rec_nat c h n) ==> f 0 = c"
1.20  by simp
1.21
1.22 -lemma def_nat_rec_Suc: "(!!n. f n == nat_rec c h n) ==> f (Suc n) = h n (f n)"
1.23 +lemma def_rec_nat_Suc: "(!!n. f n == rec_nat c h n) ==> f (Suc n) = h n (f n)"
1.24  by simp
1.25
1.26  lemma not0_implies_Suc: "n \<noteq> 0 ==> \<exists>m. n = Suc m"
```