src/ZF/ROOT.ML

--- a/src/ZF/ROOT.ML	Tue Sep 22 13:49:22 1998 +0200
+++ b/src/ZF/ROOT.ML	Tue Sep 22 13:50:57 1998 +0200
@@ -38,9 +38,15 @@
 use     "typechk.ML";
 use_thy "InfDatatype";
 use_thy "List";
-use_thy "EquivClass";
 
-(*printing functions are inherited from FOL*)
+(*Integers & binary integer arithmetic*)
+cd "Integ";
+use_thy "Bin";
+cd "..";
+
+(*the all-in-one theory*)
+use_thy "Main";
+
 print_depth 8;
 
 Goal "True";  (*leave subgoal package empty*)