src/HOL/Main.thy
changeset 55067 a452de24a877
parent 55066 4e5ddf3162ac
child 55069 b3e44be90122
     1.1 --- a/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -24,8 +24,7 @@
     1.4    ordIso2 (infix "=o" 50) and
     1.5    csum (infixr "+c" 65) and
     1.6    cprod (infixr "*c" 80) and
     1.7 -  cexp (infixr "^c" 90) and
     1.8 -  convol ("<_ , _>")
     1.9 +  cexp (infixr "^c" 90)
    1.10  
    1.11  no_syntax (xsymbols)
    1.12    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)