src/HOL/BNF_GFP.thy
changeset 55413 a8e96847523c
parent 55079 ec08a67e993b
child 55414 eab03e9cee8a
     1.1 --- a/src/HOL/BNF_GFP.thy	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/BNF_GFP.thy	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -272,10 +272,10 @@
     1.4  lemma nat_rec_Suc_imp: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
     1.5  by auto
     1.6  
     1.7 -lemma list_rec_Nil_imp: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
     1.8 +lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
     1.9  by auto
    1.10  
    1.11 -lemma list_rec_Cons_imp: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
    1.12 +lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
    1.13  by auto
    1.14  
    1.15  lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"