src/ZF/ROOT.ML
changeset 9211 6236c5285bd8
parent 9176 8f975d9c1046
child 9548 15bee2731e43
     1.1 --- a/src/ZF/ROOT.ML	Fri Jun 30 12:49:11 2000 +0200
     1.2 +++ b/src/ZF/ROOT.ML	Fri Jun 30 12:51:30 2000 +0200
     1.3 @@ -18,7 +18,6 @@
     1.4  (*Add user sections for inductive/datatype definitions*)
     1.5  use     "thy_syntax";
     1.6  
     1.7 -use_thy "Let";
     1.8  use_thy "ZF";
     1.9  use     "Tools/typechk";
    1.10  use_thy "mono";
    1.11 @@ -28,7 +27,6 @@
    1.12  use     "Tools/inductive_package";
    1.13  use     "Tools/induct_tacs";
    1.14  use     "Tools/primrec_package";
    1.15 -use_thy "Inductive";
    1.16  use_thy "QUniv";
    1.17  use     "Tools/datatype_package";
    1.18