src/HOL/ROOT.ML
changeset 1470 49b3e075f124
parent 1358 0b63af4a2627
child 1496 c443b2adaf52
     1.1 --- a/src/HOL/ROOT.ML	Thu Feb 01 12:08:43 1996 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Thu Feb 01 13:25:40 1996 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4  use_thy "Ord";
     1.5  use_thy "subset";
     1.6  use     "hologic.ML";
     1.7 -use     "subtype.ML";
     1.8 +use     "typedef.ML";
     1.9  use_thy "Prod";
    1.10  use_thy "Sum";
    1.11  use_thy "Gfp";