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

diff -r 2eb142800801 -r e24f47f8938e src/ZF/Makefile
--- a/src/ZF/Makefile	Mon Aug 15 19:01:51 1994 +0200
+++ b/src/ZF/Makefile	Tue Aug 16 18:53:29 1994 +0200
@@ -24,9 +24,10 @@
 	equalities.thy equalities.ML Bool.thy Bool.ML \
 	Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \
 	ind_syntax.thy ind_syntax.ML add_ind_def.thy add_ind_def.ML \
-\       intr_elim.thy intr_elim.ML indrule.thy indrule.ML \
+	intr_elim.thy intr_elim.ML indrule.thy indrule.ML \
 	inductive.thy inductive.ML \
-	Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \
+	Perm.thy Perm.ML Rel.thy Rel.ML EquivClass.ML EquivClass.thy \
+	Trancl.thy Trancl.ML \
 	WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \
 	Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \
 	QUniv.thy QUniv.ML constructor.ML Datatype.thy Datatype.ML  \
@@ -40,7 +41,7 @@
             IMP/Denotation.thy IMP/Equiv.ML IMP/Equiv.thy
 
 EX_FILES = ex/ROOT.ML ex/misc.ML ex/Ramsey.ML ex/Ramsey.thy\
-	   ex/Equiv.ML ex/Equiv.thy ex/Integ.ML ex/Integ.thy\
+	   ex/Integ.ML ex/Integ.thy\
            ex/twos_compl.ML ex/Bin.thy ex/Bin.ML\
 	   ex/BT.thy ex/BT.ML ex/Term.thy ex/Term.ML \
 	   ex/TF.thy ex/TF.ML ex/Ntree.thy ex/Ntree.ML \