src/HOL/Main.thy
changeset 55065 6d0af3c10864
parent 55062 6d3fad6f01c9
child 55066 4e5ddf3162ac
     1.1 --- a/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -18,10 +18,10 @@
     1.4    sup (infixl "\<squnion>" 65) and
     1.5    Inf ("\<Sqinter>_" [900] 900) and
     1.6    Sup ("\<Squnion>_" [900] 900) and
     1.7 -  ordLeq2 ("<=o") and
     1.8 -  ordLeq3 ("\<le>o") and
     1.9 -  ordLess2 ("<o") and
    1.10 -  ordIso2 ("=o") and
    1.11 +  ordLeq2 (infix "<=o" 50) and
    1.12 +  ordLeq3 (infix "\<le>o" 50) and
    1.13 +  ordLess2 (infix "<o" 50) and
    1.14 +  ordIso2 (infix "=o" 50) and
    1.15    csum (infixr "+c" 65) and
    1.16    cprod (infixr "*c" 80) and
    1.17    cexp (infixr "^c" 90)