--- a/src/HOL/ROOT.ML Wed Nov 12 16:27:13 1997 +0100
+++ b/src/HOL/ROOT.ML Wed Nov 12 16:28:53 1997 +0100
@@ -13,15 +13,15 @@
print_depth 1;
(* Add user sections *)
-use "../Pure/section_utils.ML";
+use "$ISABELLE_HOME/src/Pure/section_utils.ML";
use "thy_syntax.ML";
-use "../Provers/simplifier.ML";
-use "../Provers/splitter.ML";
-use "../Provers/hypsubst.ML";
-use "../Provers/classical.ML";
-use "../Provers/blast.ML";
-use "../Provers/nat_transitive.ML";
+use "$ISABELLE_HOME/src/Provers/simplifier.ML";
+use "$ISABELLE_HOME/src/Provers/splitter.ML";
+use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
+use "$ISABELLE_HOME/src/Provers/classical.ML";
+use "$ISABELLE_HOME/src/Provers/blast.ML";
+use "$ISABELLE_HOME/src/Provers/nat_transitive.ML";
use "thy_data.ML";
@@ -32,7 +32,7 @@
use_thy "Ord";
use_thy "subset";
-use "typedef.ML";
+use "typedef.ML";
use_thy "Sum";
use_thy "Gfp";