src/HOL/HOL.thy
changeset 28952 15a4b2cf8c34
parent 28856 5e009a80fe6d
child 29105 8f38bf68d42e
     1.1 --- a/src/HOL/HOL.thy	Wed Dec 03 09:53:58 2008 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Dec 03 15:58:44 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/HOL.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
     1.7  *)
     1.8  
     1.9 @@ -8,7 +7,7 @@
    1.10  theory HOL
    1.11  imports Pure
    1.12  uses
    1.13 -  ("hologic.ML")
    1.14 +  ("Tools/hologic.ML")
    1.15    "~~/src/Tools/IsaPlanner/zipper.ML"
    1.16    "~~/src/Tools/IsaPlanner/isand.ML"
    1.17    "~~/src/Tools/IsaPlanner/rw_tools.ML"
    1.18 @@ -22,7 +21,7 @@
    1.19    "~~/src/Provers/coherent.ML"
    1.20    "~~/src/Provers/eqsubst.ML"
    1.21    "~~/src/Provers/quantifier1.ML"
    1.22 -  ("simpdata.ML")
    1.23 +  ("Tools/simpdata.ML")
    1.24    "~~/src/Tools/random_word.ML"
    1.25    "~~/src/Tools/atomize_elim.ML"
    1.26    "~~/src/Tools/induct.ML"
    1.27 @@ -801,7 +800,7 @@
    1.28    and [sym] = sym not_sym
    1.29    and [Pure.elim?] = iffD1 iffD2 impE
    1.30  
    1.31 -use "hologic.ML"
    1.32 +use "Tools/hologic.ML"
    1.33  
    1.34  
    1.35  subsubsection {* Atomizing meta-level connectives *}
    1.36 @@ -1285,7 +1284,7 @@
    1.37    "(\<exists>x y. P x y) = (\<exists>y x. P x y)"
    1.38    by blast
    1.39  
    1.40 -use "simpdata.ML"
    1.41 +use "Tools/simpdata.ML"
    1.42  ML {* open Simpdata *}
    1.43  
    1.44  setup {*