# HG changeset patch
# User wenzelm
# Date 796655329 -7200
# Node ID b5e3fa9664fed5b038cf58f612b7a9fc45206857
# Parent  eab3015d97f035271ddcb7068837e6ccd1ff7593
replaced 'arities' by 'instance';

diff -r eab3015d97f0 -r b5e3fa9664fe src/HOL/Integ/Integ.thy
--- a/src/HOL/Integ/Integ.thy	Fri Mar 31 12:22:16 1995 +0200
+++ b/src/HOL/Integ/Integ.thy	Fri Mar 31 15:08:49 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)