src/HOL/BNF_GFP.thy
changeset 55415 05f5fdb8d093
parent 55414 eab03e9cee8a
child 55463 942c2153b5b4
     1.1 --- a/src/HOL/BNF_GFP.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/BNF_GFP.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -266,10 +266,10 @@
     1.4  lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
     1.5  unfolding Field_card_of csum_def by auto
     1.6  
     1.7 -lemma nat_rec_0_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
     1.8 +lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
     1.9  by auto
    1.10  
    1.11 -lemma nat_rec_Suc_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
    1.12 +lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
    1.13  by auto
    1.14  
    1.15  lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"