src/HOL/Main.thy
changeset 55066 4e5ddf3162ac
parent 55065 6d0af3c10864
child 55067 a452de24a877
--- a/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -24,7 +24,8 @@
   ordIso2 (infix "=o" 50) and
   csum (infixr "+c" 65) and
   cprod (infixr "*c" 80) and
-  cexp (infixr "^c" 90)
+  cexp (infixr "^c" 90) and
+  convol ("<_ , _>")
 
 no_syntax (xsymbols)
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)