src/HOL/Main.thy
changeset 55086 500ef036117b
parent 55079 ec08a67e993b
child 55087 252c7fec4119
     1.1 --- a/src/HOL/Main.thy	Mon Jan 20 21:32:41 2014 +0100
     1.2 +++ b/src/HOL/Main.thy	Mon Jan 20 21:45:08 2014 +0100
     1.3 @@ -30,7 +30,8 @@
     1.4    card_of ("|_|") and
     1.5    csum (infixr "+c" 65) and
     1.6    cprod (infixr "*c" 80) and
     1.7 -  cexp (infixr "^c" 90)
     1.8 +  cexp (infixr "^c" 90) and
     1.9 +  convol ("<_ , _>")
    1.10  
    1.11  no_syntax (xsymbols)
    1.12    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)