Now hologic.ML is loaded in HOL.ML
authorpaulson
Thu Sep 12 10:35:11 1996 +0200 (1996-09-12)
changeset 198238aafcab6890
parent 1981 432db3edccdc
child 1983 f3f7bf0079fa
Now hologic.ML is loaded in HOL.ML
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/ROOT.ML	Thu Sep 12 10:34:21 1996 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Thu Sep 12 10:35:11 1996 +0200
     1.3 @@ -22,10 +22,8 @@
     1.4  
     1.5  
     1.6  use_thy "HOL";
     1.7 -
     1.8  use_thy "Ord";
     1.9  use_thy "subset";
    1.10 -use     "hologic.ML";
    1.11  use     "typedef.ML";
    1.12  use_thy "Sum";
    1.13  use_thy "Gfp";