src/HOL/BNF_Examples/Stream_Processor.thy

 
 section {* Generalization to an Arbitrary BNF as Codomain *}
 
 bnf_axiomatization ('a, 'b) F for map: F
 
-notation BNF_Def.convol ("<_ , _>")
+notation BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
 
 definition \<theta> :: "('p,'a) F * 'b \<Rightarrow> ('p,'a * 'b) F" where
-  "\<theta> xb = F id <id, \<lambda> a. (snd xb)> (fst xb)"
+  "\<theta> xb = F id \<langle>id, \<lambda> a. (snd xb)\<rangle> (fst xb)"
 
 (* The strength laws for \<theta>: *)
 lemma \<theta>_natural: "F id (map_prod f g) o \<theta> = \<theta> o map_prod (F id f) g"
   unfolding \<theta>_def F.map_comp comp_def id_apply convol_def map_prod_def split_beta fst_conv snd_conv ..