hide BNF notation
authorblanchet
Mon, 20 Jan 2014 21:45:08 +0100
changeset 55086 500ef036117b
parent 55085 0e8e4dc55866
child 55087 252c7fec4119
hide BNF notation
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)