src/ZF/ROOT.ML
changeset 5529 4a54acae6a15
parent 5511 7f52fb755581
child 6053 8a1059aa01f0
     1.1 --- a/src/ZF/ROOT.ML	Tue Sep 22 13:49:22 1998 +0200
     1.2 +++ b/src/ZF/ROOT.ML	Tue Sep 22 13:50:57 1998 +0200
     1.3 @@ -38,9 +38,15 @@
     1.4  use     "typechk.ML";
     1.5  use_thy "InfDatatype";
     1.6  use_thy "List";
     1.7 -use_thy "EquivClass";
     1.8  
     1.9 -(*printing functions are inherited from FOL*)
    1.10 +(*Integers & binary integer arithmetic*)
    1.11 +cd "Integ";
    1.12 +use_thy "Bin";
    1.13 +cd "..";
    1.14 +
    1.15 +(*the all-in-one theory*)
    1.16 +use_thy "Main";
    1.17 +
    1.18  print_depth 8;
    1.19  
    1.20  Goal "True";  (*leave subgoal package empty*)