src/HOL/ROOT.ML

-(*  Title:      CHOL/ROOT.ML
+(*  Title:      HOL/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1993  University of Cambridge
 
 Adds Classical Higher-order Logic to a database containing Pure Isabelle.

 (* Add user sections *)
 use "../Pure/section_utils.ML";
 use "thy_syntax.ML";
 
 use_thy "HOL";
-use "../Provers/simplifier.ML";
 use "../Provers/splitter.ML";
 use "../Provers/hypsubst.ML";
 use "../Provers/classical.ML";
 
 (** Applying HypsubstFun to generate hyp_subst_tac **)

                      addSEs [exE,ex1E] addEs [allE];
 
 use     "simpdata.ML";
 use_thy "Ord";
 use_thy "subset";
-use_thy "equalities";
 use     "hologic.ML";
 use     "subtype.ML";
 use_thy "Prod";
 use_thy "Sum";
 use_thy "Gfp";