src/ZF/Ordinal.thy
changeset 22808 a7daa74e2980
parent 16417 9bc16273c2d4
child 24893 b8ef7afe3a6b
     1.1 --- a/src/ZF/Ordinal.thy	Thu Apr 26 13:33:17 2007 +0200
     1.2 +++ b/src/ZF/Ordinal.thy	Thu Apr 26 14:24:08 2007 +0200
     1.3 @@ -26,16 +26,15 @@
     1.4    Limit         :: "i=>o"
     1.5      "Limit(i)    == Ord(i) & 0<i & (ALL y. y<i --> succ(y)<i)"
     1.6  
     1.7 -syntax
     1.8 -  "le"          :: "[i,i] => o"  (infixl 50)   (*less-than or equals*)
     1.9 +abbreviation
    1.10 +  le  (infixl "le" 50) where
    1.11 +  "x le y == x < succ(y)"
    1.12  
    1.13 -translations
    1.14 -  "x le y"      == "x < succ(y)"
    1.15 +notation (xsymbols)
    1.16 +  le  (infixl "\<le>" 50)
    1.17  
    1.18 -syntax (xsymbols)
    1.19 -  "op le"       :: "[i,i] => o"  (infixl "\<le>" 50)  (*less-than or equals*)
    1.20 -syntax (HTML output)
    1.21 -  "op le"       :: "[i,i] => o"  (infixl "\<le>" 50)  (*less-than or equals*)
    1.22 +notation (HTML output)
    1.23 +  le  (infixl "\<le>" 50)
    1.24  
    1.25  
    1.26  subsection{*Rules for Transset*}