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)