# HG changeset patch
# User lcp
# Date 777056322 -7200
# Node ID 851df239ac8b7dffd07408917bc1967d83e5a22f
# Parent  e24f47f8938e66c058a0e1f4dc13f337df435e16
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass

diff -r e24f47f8938e -r 851df239ac8b src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Tue Aug 16 18:53:29 1994 +0200
+++ b/src/ZF/ROOT.ML	Tue Aug 16 18:58:42 1994 +0200
@@ -42,6 +42,7 @@
 
 use_thy "InfDatatype";
 use_thy "List";
+use_thy "EquivClass";
 
 (*printing functions are inherited from FOL*)
 print_depth 8;
diff -r e24f47f8938e -r 851df239ac8b src/ZF/ex/Integ.thy
--- a/src/ZF/ex/Integ.thy	Tue Aug 16 18:53:29 1994 +0200
+++ b/src/ZF/ex/Integ.thy	Tue Aug 16 18:58:42 1994 +0200
@@ -6,7 +6,7 @@
 The integers as equivalence classes over nat*nat.
 *)
 
-Integ = Equiv + Arith +
+Integ = EquivClass + Arith +
 consts
     intrel,integ::      "i"
     znat	::	"i=>i"		("$# _" [80] 80)