src/ZF/Integ/Int.thy

--- a/src/ZF/Integ/Int.thy	Thu Jul 13 23:26:08 2000 +0200
+++ b/src/ZF/Integ/Int.thy	Fri Jul 14 13:39:03 2000 +0200
@@ -26,7 +26,7 @@
      "intrel == {p:(nat*nat)*(nat*nat).                 
         EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
 
-    int_def   "int == (nat*nat)/intrel"
+    int_def   "int == (nat*nat)//intrel"
     
     int_of_def  "$# m == intrel `` {<m,0>}"