src/ZF/ROOT.ML
changeset 484 70b789956bd3
parent 435 ca5356bd315a
child 488 52f7447d4f1b
--- a/src/ZF/ROOT.ML	Thu Jul 21 16:51:26 1994 +0200
+++ b/src/ZF/ROOT.ML	Tue Jul 26 13:21:20 1994 +0200
@@ -28,8 +28,7 @@
 
 print_depth 1;
 
-use_thy "CardinalArith";
-use_thy "Fin";
+use_thy "Cardinal_AC";
 use_thy "ListFn";
 
 (*printing functions are inherited from FOL*)