# HG changeset patch
# User blanchet
# Date 1390250708 -3600
# Node ID 500ef036117ba64fe2f8c896bde32ba8b1cf23ec
# Parent  0e8e4dc558664de0e71ca8cf1c6638af3e5184cd
hide BNF notation

diff -r 0e8e4dc55866 -r 500ef036117b src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Jan 20 21:32:41 2014 +0100
+++ b/src/HOL/Main.thy	Mon Jan 20 21:45:08 2014 +0100
@@ -30,7 +30,8 @@
   card_of ("|_|") 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)