src/HOL/BNF_FP_Base.thy
changeset 57641 dc59f147b27d
parent 57525 f9dd8a33f820
child 57698 afef6616cbae
     1.1 --- a/src/HOL/BNF_FP_Base.thy	Thu Jul 24 11:51:22 2014 +0200
     1.2 +++ b/src/HOL/BNF_FP_Base.thy	Thu Jul 24 11:54:15 2014 +0200
     1.3 @@ -113,13 +113,13 @@
     1.4  lemma rewriteL_comp_comp2: "\<lbrakk>f \<circ> g = l1 \<circ> l2; l2 \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l1 \<circ> r"
     1.5    unfolding comp_def fun_eq_iff by auto
     1.6  
     1.7 -lemma convol_o: "<f, g> \<circ> h = <f \<circ> h, g \<circ> h>"
     1.8 +lemma convol_o: "\<langle>f, g\<rangle> \<circ> h = \<langle>f \<circ> h, g \<circ> h\<rangle>"
     1.9    unfolding convol_def by auto
    1.10  
    1.11 -lemma map_prod_o_convol: "map_prod h1 h2 \<circ> <f, g> = <h1 \<circ> f, h2 \<circ> g>"
    1.12 +lemma map_prod_o_convol: "map_prod h1 h2 \<circ> \<langle>f, g\<rangle> = \<langle>h1 \<circ> f, h2 \<circ> g\<rangle>"
    1.13    unfolding convol_def by auto
    1.14  
    1.15 -lemma map_prod_o_convol_id: "(map_prod f id \<circ> <id , g>) x = <id \<circ> f , g> x"
    1.16 +lemma map_prod_o_convol_id: "(map_prod f id \<circ> \<langle>id, g\<rangle>) x = \<langle>id \<circ> f, g\<rangle> x"
    1.17    unfolding map_prod_o_convol id_comp comp_id ..
    1.18  
    1.19  lemma o_case_sum: "h \<circ> case_sum f g = case_sum (h \<circ> f) (h \<circ> g)"