author | blanchet |
Mon, 20 Jan 2014 21:45:08 +0100 | |
changeset 55086 | 500ef036117b |
parent 55085 | 0e8e4dc55866 |
child 55087 | 252c7fec4119 |
src/HOL/Main.thy | file | annotate | diff | comparison | revisions |
--- 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)