src/HOL/ROOT.ML
changeset 1264 3eb91524b938
parent 1165 97b2bb5d43c3
child 1273 6960ec882bca
--- a/src/HOL/ROOT.ML	Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/ROOT.ML	Wed Oct 04 13:10:03 1995 +0100
@@ -1,4 +1,4 @@
-(*  Title:      CHOL/ROOT.ML
+(*  Title:      HOL/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1993  University of Cambridge
@@ -18,7 +18,6 @@
 use "thy_syntax.ML";
 
 use_thy "HOL";
-use "../Provers/simplifier.ML";
 use "../Provers/splitter.ML";
 use "../Provers/hypsubst.ML";
 use "../Provers/classical.ML";
@@ -64,7 +63,6 @@
 use     "simpdata.ML";
 use_thy "Ord";
 use_thy "subset";
-use_thy "equalities";
 use     "hologic.ML";
 use     "subtype.ML";
 use_thy "Prod";