src/HOL/ROOT.ML
changeset 1496 c443b2adaf52
parent 1470 49b3e075f124
child 1515 4ed79ebab64d
     1.1 --- a/src/HOL/ROOT.ML	Tue Feb 13 17:16:06 1996 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Thu Feb 15 08:10:36 1996 +0100
     1.3 @@ -27,10 +27,9 @@
     1.4  use_thy "subset";
     1.5  use     "hologic.ML";
     1.6  use     "typedef.ML";
     1.7 -use_thy "Prod";
     1.8  use_thy "Sum";
     1.9  use_thy "Gfp";
    1.10 -use_thy "Nat";
    1.11 +use_thy "RelPow";
    1.12  
    1.13  use "datatype.ML";
    1.14  use "ind_syntax.ML";