simplified slightly by using dependencies better in theories
authorpaulson
Wed Jun 28 11:00:13 2000 +0200 (2000-06-28)
changeset 91768f975d9c1046
parent 9175 6f8499d86d4f
child 9177 199b43f712af
simplified slightly by using dependencies better in theories
src/ZF/ROOT.ML
     1.1 --- a/src/ZF/ROOT.ML	Wed Jun 28 10:58:06 2000 +0200
     1.2 +++ b/src/ZF/ROOT.ML	Wed Jun 28 11:00:13 2000 +0200
     1.3 @@ -26,22 +26,14 @@
     1.4  use     "Tools/cartprod";
     1.5  use_thy "Fixedpt";
     1.6  use     "Tools/inductive_package";
     1.7 -use_thy "Inductive";
     1.8  use     "Tools/induct_tacs";
     1.9  use     "Tools/primrec_package";
    1.10 +use_thy "Inductive";
    1.11  use_thy "QUniv";
    1.12  use     "Tools/datatype_package";
    1.13 -use_thy "Datatype";
    1.14 -use_thy "InfDatatype";
    1.15 -use_thy "List";
    1.16 -
    1.17 -(*Integers & binary integer arithmetic*)
    1.18 -cd "Integ";
    1.19 -use_thy "Bin";
    1.20 -cd "..";
    1.21  
    1.22  (*the all-in-one theory*)
    1.23 -use_thy "Main";
    1.24 +with_path "Integ" use_thy "Main";
    1.25  
    1.26  simpset_ref() := simpset() setmksimps (map mk_eq o Ord_atomize o gen_all);
    1.27