1.1 --- a/src/HOL/Main.thy	Mon Jan 20 18:24:55 2014 +0100
     1.2 +++ b/src/HOL/Main.thy	Mon Jan 20 18:24:55 2014 +0100
     1.3 @@ -17,7 +17,14 @@
     1.4    inf (infixl "\<sqinter>" 70) and
     1.5    sup (infixl "\<squnion>" 65) and
     1.6    Inf ("\<Sqinter>_" [900] 900) and
     1.7 -  Sup ("\<Squnion>_" [900] 900)
     1.8 +  Sup ("\<Squnion>_" [900] 900) and
     1.9 +  ordLeq2 ("<=o") and
    1.10 +  ordLeq3 ("\<le>o") and
    1.11 +  ordLess2 ("<o") and
    1.12 +  ordIso2 ("=o") and
    1.13 +  csum (infixr "+c" 65) and
    1.14 +  cprod (infixr "*c" 80) and
    1.15 +  cexp (infixr "^c" 90)
    1.16  
    1.17  no_syntax (xsymbols)
    1.18    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)