src/HOL/ROOT.ML
changeset 4088 9be9e39fd862
parent 4024 3c056eab237c
child 4222 d7573d6d0513
     1.1 --- a/src/HOL/ROOT.ML	Mon Nov 03 12:11:34 1997 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Mon Nov 03 12:12:10 1997 +0100
     1.3 @@ -23,8 +23,13 @@
     1.4  use "../Provers/blast.ML";
     1.5  use "../Provers/nat_transitive.ML";
     1.6  
     1.7 +use "thy_data.ML";
     1.8  
     1.9  use_thy "HOL";
    1.10 +use "hologic.ML";
    1.11 +use "cladata.ML";
    1.12 +use "simpdata.ML";
    1.13 +
    1.14  use_thy "Ord";
    1.15  use_thy "subset";
    1.16  use     "typedef.ML";
    1.17 @@ -34,8 +39,8 @@
    1.18  use "datatype.ML";
    1.19  use "ind_syntax.ML";
    1.20  use "add_ind_def.ML";
    1.21 -use "intr_elim.ML";
    1.22 -use "indrule.ML";
    1.23 +use_thy "intr_elim";
    1.24 +use_thy "indrule";
    1.25  use_thy "Inductive";
    1.26  
    1.27  use_thy "RelPow";