changeset 55086 | 500ef036117b |
parent 55079 | ec08a67e993b |
child 55087 | 252c7fec4119 |
--- 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)