# HG changeset patch
# User wenzelm
# Date 879348533 -3600
# Node ID d7573d6d051307d20250abb9c1bffecc3afa8d40
# Parent  ed0f67fb458ba30ba54d8f0063c125469c3a6c97
refer to $ISABELLE_HOME/src;

diff -r ed0f67fb458b -r d7573d6d0513 src/CTT/ROOT.ML
--- a/src/CTT/ROOT.ML	Wed Nov 12 16:27:13 1997 +0100
+++ b/src/CTT/ROOT.ML	Wed Nov 12 16:28:53 1997 +0100
@@ -15,7 +15,7 @@
 print_depth 1;  
 
 use_thy "CTT";
-use "../Provers/typedsimp.ML";
+use "$ISABELLE_HOME/src/Provers/typedsimp.ML";
 use "rew.ML";
 use_thy "Arith";
 use_thy "Bool";
diff -r ed0f67fb458b -r d7573d6d0513 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Wed Nov 12 16:27:13 1997 +0100
+++ b/src/FOL/ROOT.ML	Wed Nov 12 16:28:53 1997 +0100
@@ -13,12 +13,12 @@
 
 print_depth 1;  
 
-use "../Provers/simplifier.ML";
-use "../Provers/splitter.ML";
-use "../Provers/ind.ML";
-use "../Provers/hypsubst.ML";
-use "../Provers/classical.ML";
-use "../Provers/blast.ML";
+use "$ISABELLE_HOME/src/Provers/simplifier.ML";
+use "$ISABELLE_HOME/src/Provers/splitter.ML";
+use "$ISABELLE_HOME/src/Provers/ind.ML";
+use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
+use "$ISABELLE_HOME/src/Provers/classical.ML";
+use "$ISABELLE_HOME/src/Provers/blast.ML";
 
 use_thy "IFOL";
 
diff -r ed0f67fb458b -r d7573d6d0513 src/HOL/ROOT.ML
--- 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";