# HG changeset patch
# User wenzelm
# Date 878555530 -3600
# Node ID 9be9e39fd86228559cfe1750a0aafbb5c8de3515
# Parent  42229596565cf80986f007c60db0934e5bfdfe1c
added thy_data;
misc fixes;

diff -r 42229596565c -r 9be9e39fd862 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Mon Nov 03 12:11:34 1997 +0100
+++ b/src/HOL/ROOT.ML	Mon Nov 03 12:12:10 1997 +0100
@@ -23,8 +23,13 @@
 use "../Provers/blast.ML";
 use "../Provers/nat_transitive.ML";
 
+use "thy_data.ML";
 
 use_thy "HOL";
+use "hologic.ML";
+use "cladata.ML";
+use "simpdata.ML";
+
 use_thy "Ord";
 use_thy "subset";
 use     "typedef.ML";
@@ -34,8 +39,8 @@
 use "datatype.ML";
 use "ind_syntax.ML";
 use "add_ind_def.ML";
-use "intr_elim.ML";
-use "indrule.ML";
+use_thy "intr_elim";
+use_thy "indrule";
 use_thy "Inductive";
 
 use_thy "RelPow";