src/ZF/ex/integ.thy

--- a/src/ZF/ex/integ.thy	Tue Oct 05 17:27:05 1993 +0100
+++ b/src/ZF/ex/integ.thy	Tue Oct 05 17:49:23 1993 +0100
@@ -33,7 +33,7 @@
     zminus_def	"$~ Z == UN p:Z. split(%x y. intrel``{<y,x>}, p)"
     
     znegative_def
-	"znegative(Z) == EX x y. x:y & y:nat & <x,y>:Z"
+	"znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
     
     zmagnitude_def
 	"zmagnitude(Z) == UN p:Z. split(%x y. (y#-x) #+ (x#-y), p)"