1.1 --- a/src/HOL/BNF_Def.thy	Thu Jul 24 11:51:22 2014 +0200
     1.2 +++ b/src/HOL/BNF_Def.thy	Thu Jul 24 11:54:15 2014 +0200
     1.3 @@ -53,21 +53,21 @@
     1.4  lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)"
     1.5    by (rule ext) (auto simp only: comp_apply collect_def)
     1.6  
     1.7 -definition convol ("<_ , _>") where
     1.8 -"<f , g> \<equiv> %a. (f a, g a)"
     1.9 +definition convol ("\<langle>(_,/ _)\<rangle>") where
    1.10 +"\<langle>f, g\<rangle> \<equiv> \<lambda>a. (f a, g a)"
    1.11  
    1.12  lemma fst_convol:
    1.13 -"fst \<circ> <f , g> = f"
    1.14 +"fst \<circ> \<langle>f, g\<rangle> = f"
    1.15  apply(rule ext)
    1.16  unfolding convol_def by simp
    1.17  
    1.18  lemma snd_convol:
    1.19 -"snd \<circ> <f , g> = g"
    1.20 +"snd \<circ> \<langle>f, g\<rangle> = g"
    1.21  apply(rule ext)
    1.22  unfolding convol_def by simp
    1.23  
    1.24  lemma convol_mem_GrpI:
    1.25 -"x \<in> A \<Longrightarrow> <id , g> x \<in> (Collect (split (Grp A g)))"
    1.26 +"x \<in> A \<Longrightarrow> \<langle>id, g\<rangle> x \<in> (Collect (split (Grp A g)))"
    1.27  unfolding convol_def Grp_def by auto
    1.28  
    1.29  definition csquare where
    1.30 @@ -182,7 +182,7 @@
    1.31  lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)"
    1.32    unfolding rel_fun_def vimage2p_def by auto
    1.33  
    1.34 -lemma convol_image_vimage2p: "<f \<circ> fst, g \<circ> snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
    1.35 +lemma convol_image_vimage2p: "\<langle>f \<circ> fst, g \<circ> snd\<rangle> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
    1.36    unfolding vimage2p_def convol_def by auto
    1.37  
    1.38  lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"

     2.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy	Thu Jul 24 11:51:22 2014 +0200
     2.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy	Thu Jul 24 11:54:15 2014 +0200
     2.3 @@ -11,11 +11,11 @@
     2.4  imports "~~/src/HOL/Library/FSet"
     2.5  begin
     2.6  
     2.7 -notation BNF_Def.convol ("<_ , _>")
     2.8 +notation BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
     2.9  
    2.10  declare fset_to_fset[simp]
    2.11  
    2.12 -lemma fst_snd_convol_o[simp]: "<fst o s, snd o s> = s"
    2.13 +lemma fst_snd_convol_o[simp]: "\<langle>fst o s, snd o s\<rangle> = s"
    2.14  apply(rule ext) by (simp add: convol_def)
    2.15  
    2.16  abbreviation sm_abbrev (infix "\<oplus>" 60)

     3.1 --- a/src/HOL/BNF_Examples/Stream_Processor.thy	Thu Jul 24 11:51:22 2014 +0200
     3.2 +++ b/src/HOL/BNF_Examples/Stream_Processor.thy	Thu Jul 24 11:54:15 2014 +0200
     3.3 @@ -152,10 +152,10 @@
     3.4  
     3.5  bnf_axiomatization ('a, 'b) F for map: F
     3.6  
     3.7 -notation BNF_Def.convol ("<_ , _>")
     3.8 +notation BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
     3.9  
    3.10  definition \<theta> :: "('p,'a) F * 'b \<Rightarrow> ('p,'a * 'b) F" where
    3.11 -  "\<theta> xb = F id <id, \<lambda> a. (snd xb)> (fst xb)"
    3.12 +  "\<theta> xb = F id \<langle>id, \<lambda> a. (snd xb)\<rangle> (fst xb)"
    3.13  
    3.14  (* The strength laws for \<theta>: *)
    3.15  lemma \<theta>_natural: "F id (map_prod f g) o \<theta> = \<theta> o map_prod (F id f) g"

     4.1 --- a/src/HOL/BNF_FP_Base.thy	Thu Jul 24 11:51:22 2014 +0200
     4.2 +++ b/src/HOL/BNF_FP_Base.thy	Thu Jul 24 11:54:15 2014 +0200
     4.3 @@ -113,13 +113,13 @@
     4.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"
     4.5    unfolding comp_def fun_eq_iff by auto
     4.6  
     4.7 -lemma convol_o: "<f, g> \<circ> h = <f \<circ> h, g \<circ> h>"
     4.8 +lemma convol_o: "\<langle>f, g\<rangle> \<circ> h = \<langle>f \<circ> h, g \<circ> h\<rangle>"
     4.9    unfolding convol_def by auto
    4.10  
    4.11 -lemma map_prod_o_convol: "map_prod h1 h2 \<circ> <f, g> = <h1 \<circ> f, h2 \<circ> g>"
    4.12 +lemma map_prod_o_convol: "map_prod h1 h2 \<circ> \<langle>f, g\<rangle> = \<langle>h1 \<circ> f, h2 \<circ> g\<rangle>"
    4.13    unfolding convol_def by auto
    4.14  
    4.15 -lemma map_prod_o_convol_id: "(map_prod f id \<circ> <id , g>) x = <id \<circ> f , g> x"
    4.16 +lemma map_prod_o_convol_id: "(map_prod f id \<circ> \<langle>id, g\<rangle>) x = \<langle>id \<circ> f, g\<rangle> x"
    4.17    unfolding map_prod_o_convol id_comp comp_id ..
    4.18  
    4.19  lemma o_case_sum: "h \<circ> case_sum f g = case_sum (h \<circ> f) (h \<circ> g)"

     5.1 --- a/src/HOL/BNF_LFP.thy	Thu Jul 24 11:51:22 2014 +0200
     5.2 +++ b/src/HOL/BNF_LFP.thy	Thu Jul 24 11:54:15 2014 +0200
     5.3 @@ -41,23 +41,23 @@
     5.4  lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
     5.5  unfolding Field_def by auto
     5.6  
     5.7 -lemma fst_convol': "fst (<f, g> x) = f x"
     5.8 +lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x"
     5.9  using fst_convol unfolding convol_def by simp
    5.10  
    5.11 -lemma snd_convol': "snd (<f, g> x) = g x"
    5.12 +lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x"
    5.13  using snd_convol unfolding convol_def by simp
    5.14  
    5.15 -lemma convol_expand_snd: "fst o f = g \<Longrightarrow>  <g, snd o f> = f"
    5.16 +lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f"
    5.17  unfolding convol_def by auto
    5.18  
    5.19  lemma convol_expand_snd':
    5.20    assumes "(fst o f = g)"
    5.21 -  shows "h = snd o f \<longleftrightarrow> <g, h> = f"
    5.22 +  shows "h = snd o f \<longleftrightarrow> \<langle>g, h\<rangle> = f"
    5.23  proof -
    5.24 -  from assms have *: "<g, snd o f> = f" by (rule convol_expand_snd)
    5.25 -  then have "h = snd o f \<longleftrightarrow> h = snd o <g, snd o f>" by simp
    5.26 +  from assms have *: "\<langle>g, snd o f\<rangle> = f" by (rule convol_expand_snd)
    5.27 +  then have "h = snd o f \<longleftrightarrow> h = snd o \<langle>g, snd o f\<rangle>" by simp
    5.28    moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol)
    5.29 -  moreover have "\<dots> \<longleftrightarrow> <g, h> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
    5.30 +  moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
    5.31    ultimately show ?thesis by simp
    5.32  qed
    5.33  lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"

     6.1 --- a/src/HOL/Main.thy	Thu Jul 24 11:51:22 2014 +0200
     6.2 +++ b/src/HOL/Main.thy	Thu Jul 24 11:54:15 2014 +0200
     6.3 @@ -26,7 +26,7 @@
     6.4    csum (infixr "+c" 65) and
     6.5    cprod (infixr "*c" 80) and
     6.6    cexp (infixr "^c" 90) and
     6.7 -  convol ("<_ , _>")
     6.8 +  convol ("\<langle>(_,/ _)\<rangle>")
     6.9  
    6.10  hide_const (open)
    6.11    czero cinfinite cfinite csum cone ctwo Csum cprod cexp