src/ZF/ex/Integ.thy
changeset 29 4ec9b266ccd1
parent 0 a5a9c433f639
child 532 851df239ac8b
     1.1 --- a/src/ZF/ex/Integ.thy	Tue Oct 05 17:27:05 1993 +0100
     1.2 +++ b/src/ZF/ex/Integ.thy	Tue Oct 05 17:49:23 1993 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4      zminus_def	"$~ Z == UN p:Z. split(%x y. intrel``{<y,x>}, p)"
     1.5      
     1.6      znegative_def
     1.7 -	"znegative(Z) == EX x y. x:y & y:nat & <x,y>:Z"
     1.8 +	"znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
     1.9      
    1.10      zmagnitude_def
    1.11  	"zmagnitude(Z) == UN p:Z. split(%x y. (y#-x) #+ (x#-y), p)"