--- 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;
--- 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)