1.1 --- a/src/HOL/Main.thy	Thu Jul 24 11:51:22 2014 +0200
     1.2 +++ b/src/HOL/Main.thy	Thu Jul 24 11:54:15 2014 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4    csum (infixr "+c" 65) and
     1.5    cprod (infixr "*c" 80) and
     1.6    cexp (infixr "^c" 90) and
     1.7 -  convol ("<_ , _>")
     1.8 +  convol ("\<langle>(_,/ _)\<rangle>")
     1.9  
    1.10  hide_const (open)
    1.11    czero cinfinite cfinite csum cone ctwo Csum cprod cexp