src/HOL/ROOT.ML
changeset 1264 3eb91524b938
parent 1165 97b2bb5d43c3
child 1273 6960ec882bca
     1.1 --- a/src/HOL/ROOT.ML	Wed Oct 04 13:01:05 1995 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Wed Oct 04 13:10:03 1995 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      CHOL/ROOT.ML
     1.5 +(*  Title:      HOL/ROOT.ML
     1.6      ID:         $Id$
     1.7      Author:     Tobias Nipkow
     1.8      Copyright   1993  University of Cambridge
     1.9 @@ -18,7 +18,6 @@
    1.10  use "thy_syntax.ML";
    1.11  
    1.12  use_thy "HOL";
    1.13 -use "../Provers/simplifier.ML";
    1.14  use "../Provers/splitter.ML";
    1.15  use "../Provers/hypsubst.ML";
    1.16  use "../Provers/classical.ML";
    1.17 @@ -64,7 +63,6 @@
    1.18  use     "simpdata.ML";
    1.19  use_thy "Ord";
    1.20  use_thy "subset";
    1.21 -use_thy "equalities";
    1.22  use     "hologic.ML";
    1.23  use     "subtype.ML";
    1.24  use_thy "Prod";