src/HOL/Library/FinFun_Syntax.thy
changeset 61955 e96292f32c3c
parent 61384 9f5145281888
child 62390 842917225d56
     1.1 --- a/src/HOL/Library/FinFun_Syntax.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Library/FinFun_Syntax.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -13,12 +13,12 @@
     1.4    finfun_const ("K$/ _" [0] 1) and
     1.5    finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
     1.6    finfun_apply (infixl "$" 999) and
     1.7 -  finfun_comp (infixr "o$" 55) and
     1.8 -  finfun_comp2 (infixr "$o" 55) and
     1.9 +  finfun_comp (infixr "\<circ>$" 55) and
    1.10 +  finfun_comp2 (infixr "$\<circ>" 55) and
    1.11    finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
    1.12  
    1.13 -notation (xsymbols) 
    1.14 -  finfun_comp (infixr "\<circ>$" 55) and
    1.15 -  finfun_comp2 (infixr "$\<circ>" 55)
    1.16 +notation (ASCII)
    1.17 +  finfun_comp (infixr "o$" 55) and
    1.18 +  finfun_comp2 (infixr "$o" 55)
    1.19  
    1.20  end
    1.21 \ No newline at end of file