src/ZF/Integ/Int.thy
changeset 9570 e16e168984e1
parent 9548 15bee2731e43
child 9578 ab26d6c8ebfe
     1.1 --- a/src/ZF/Integ/Int.thy	Thu Aug 10 00:45:23 2000 +0200
     1.2 +++ b/src/ZF/Integ/Int.thy	Thu Aug 10 11:27:34 2000 +0200
     1.3 @@ -30,7 +30,10 @@
     1.4  
     1.5    znegative   ::      i=>o
     1.6      "znegative(z) == EX x y. x<y & y:nat & <x,y>:z"
     1.7 -  
     1.8 +
     1.9 +  iszero      ::      i=>o
    1.10 +    "iszero(z) == z = $# 0"
    1.11 +    
    1.12    zmagnitude  ::      i=>i
    1.13      "zmagnitude(z) ==
    1.14       THE m. m : nat & ((~ znegative(z) & z = $# m) |
    1.15 @@ -62,7 +65,7 @@
    1.16       "z1 $< z2 == znegative(z1 $- z2)"
    1.17    
    1.18    zle          ::      [i,i]=>o      (infixl "$<=" 50)
    1.19 -     "z1 $<= z2 == z1 $< z2 | z1=z2"
    1.20 +     "z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
    1.21    
    1.22  (*div and mod await definitions!*)
    1.23  consts