hide BNF notation
authorblanchet
Mon Jan 20 21:45:08 2014 +0100 (2014-01-20)
changeset 55086500ef036117b
parent 55085 0e8e4dc55866
child 55087 252c7fec4119
hide BNF notation
src/HOL/Main.thy
     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)