src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy
changeset 57641 dc59f147b27d
parent 55931 62156e694f3d
     1.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy	Thu Jul 24 11:51:22 2014 +0200
     1.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy	Thu Jul 24 11:54:15 2014 +0200
     1.3 @@ -11,11 +11,11 @@
     1.4  imports "~~/src/HOL/Library/FSet"
     1.5  begin
     1.6  
     1.7 -notation BNF_Def.convol ("<_ , _>")
     1.8 +notation BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
     1.9  
    1.10  declare fset_to_fset[simp]
    1.11  
    1.12 -lemma fst_snd_convol_o[simp]: "<fst o s, snd o s> = s"
    1.13 +lemma fst_snd_convol_o[simp]: "\<langle>fst o s, snd o s\<rangle> = s"
    1.14  apply(rule ext) by (simp add: convol_def)
    1.15  
    1.16  abbreviation sm_abbrev (infix "\<oplus>" 60)