replaced 'arities' by 'instance';

--- a/Integ/Integ.thy	Thu Mar 30 13:39:36 1995 +0200
+++ b/Integ/Integ.thy	Fri Mar 31 15:09:21 1995 +0200
@@ -17,12 +17,11 @@
    "intrel == {p. ? x1 y1 x2 y2. p=<<x1::nat,y1>,<x2,y2>> & x1+y2 = x2+y1}"
 
 subtype (Integ)
-  int = "{x::(nat*nat).True}/intrel"		("quotient_def")
+  int = "{x::(nat*nat).True}/intrel"		(Equiv.quotient_def)
 
-arities int :: ord
-        int :: plus
-        int :: times
-        int :: minus
+instance
+  int :: {ord, plus, times, minus}
+
 consts
   zNat        :: "nat set"
   znat	      :: "nat => int"	   ("$# _" [80] 80)