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"