src/HOL/HOL.thy

 (*  Title:      HOL/HOL.thy
-    ID:         $Id$
     Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
 *)
 
 header {* The basis of Higher-Order Logic *}
 
 theory HOL
 imports Pure
 uses
-  ("hologic.ML")
+  ("Tools/hologic.ML")
   "~~/src/Tools/IsaPlanner/zipper.ML"
   "~~/src/Tools/IsaPlanner/isand.ML"
   "~~/src/Tools/IsaPlanner/rw_tools.ML"
   "~~/src/Tools/IsaPlanner/rw_inst.ML"
   "~~/src/Provers/project_rule.ML"

   "~~/src/Provers/blast.ML"
   "~~/src/Provers/clasimp.ML"
   "~~/src/Provers/coherent.ML"
   "~~/src/Provers/eqsubst.ML"
   "~~/src/Provers/quantifier1.ML"
-  ("simpdata.ML")
+  ("Tools/simpdata.ML")
   "~~/src/Tools/random_word.ML"
   "~~/src/Tools/atomize_elim.ML"
   "~~/src/Tools/induct.ML"
   ("~~/src/Tools/induct_tacs.ML")
   "~~/src/Tools/code/code_name.ML"

 
 lemmas [trans] = trans
   and [sym] = sym not_sym
   and [Pure.elim?] = iffD1 iffD2 impE
 
-use "hologic.ML"
+use "Tools/hologic.ML"
 
 
 subsubsection {* Atomizing meta-level connectives *}
 
 axiomatization where

 
 lemma ex_comm:
   "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
   by blast
 
-use "simpdata.ML"
+use "Tools/simpdata.ML"
 ML {* open Simpdata *}
 
 setup {*
   Simplifier.method_setup Splitter.split_modifiers
   #> Simplifier.map_simpset (K Simpdata.simpset_simprocs)