src/HOL/BNF_Examples/Stream_Processor.thy
changeset 57641 dc59f147b27d
parent 57634 efc00b9b8680
     1.1 --- a/src/HOL/BNF_Examples/Stream_Processor.thy	Thu Jul 24 11:51:22 2014 +0200
     1.2 +++ b/src/HOL/BNF_Examples/Stream_Processor.thy	Thu Jul 24 11:54:15 2014 +0200
     1.3 @@ -152,10 +152,10 @@
     1.4  
     1.5  bnf_axiomatization ('a, 'b) F for map: F
     1.6  
     1.7 -notation BNF_Def.convol ("<_ , _>")
     1.8 +notation BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
     1.9  
    1.10  definition \<theta> :: "('p,'a) F * 'b \<Rightarrow> ('p,'a * 'b) F" where
    1.11 -  "\<theta> xb = F id <id, \<lambda> a. (snd xb)> (fst xb)"
    1.12 +  "\<theta> xb = F id \<langle>id, \<lambda> a. (snd xb)\<rangle> (fst xb)"
    1.13  
    1.14  (* The strength laws for \<theta>: *)
    1.15  lemma \<theta>_natural: "F id (map_prod f g) o \<theta> = \<theta> o map_prod (F id f) g"