src/HOL/BNF_FP_Base.thy
changeset 55932 68c5104d2204
parent 55931 62156e694f3d
child 55936 f6591f8c629d
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Thu Mar 06 13:36:15 2014 +0100
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Thu Mar 06 13:36:48 2014 +0100
     1.3 @@ -116,11 +116,11 @@
     1.4  lemma convol_o: "<f, g> o h = <f o h, g o h>"
     1.5    unfolding convol_def by auto
     1.6  
     1.7 -lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>"
     1.8 +lemma map_prod_o_convol: "map_prod h1 h2 o <f, g> = <h1 o f, h2 o g>"
     1.9    unfolding convol_def by auto
    1.10  
    1.11 -lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
    1.12 -  unfolding map_pair_o_convol id_comp comp_id ..
    1.13 +lemma map_prod_o_convol_id: "(map_prod f id \<circ> <id , g>) x = <id \<circ> f , g> x"
    1.14 +  unfolding map_prod_o_convol id_comp comp_id ..
    1.15  
    1.16  lemma o_case_sum: "h o case_sum f g = case_sum (h o f) (h o g)"
    1.17    unfolding comp_def by (auto split: sum.splits)