src/HOL/ROOT.ML
changeset 5097 6c4a7ad6ebc7
parent 5078 7b5ea59c0275
child 5105 0ff5bec04d02
     1.1 --- a/src/HOL/ROOT.ML	Tue Jun 30 20:41:41 1998 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Tue Jun 30 20:42:47 1998 +0200
     1.3 @@ -36,8 +36,7 @@
     1.4  use_thy "Ord";
     1.5  use_thy "subset";
     1.6  use "Tools/typedef_package.ML";
     1.7 -use_thy "Sum";
     1.8 -use_thy "Gfp";
     1.9 +use_thy "Inductive";
    1.10  
    1.11  use "Tools/record_package.ML";
    1.12  use_thy "Record";
    1.13 @@ -46,11 +45,7 @@
    1.14  use_thy "Arith";
    1.15  use "arith_data.ML";
    1.16  
    1.17 -use "ind_syntax.ML";
    1.18 -use "add_ind_def.ML";
    1.19 -use_thy "intr_elim";
    1.20 -use_thy "indrule";
    1.21 -use_thy "Inductive";
    1.22 +use "Tools/inductive_package.ML";
    1.23  
    1.24  use_thy "RelPow";
    1.25  use_thy "Finite";