src/HOL/ROOT.ML
changeset 4222 d7573d6d0513
parent 4088 9be9e39fd862
child 4296 aa84d9c62454
     1.1 --- a/src/HOL/ROOT.ML	Wed Nov 12 16:27:13 1997 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Wed Nov 12 16:28:53 1997 +0100
     1.3 @@ -13,15 +13,15 @@
     1.4  print_depth 1;
     1.5  
     1.6  (* Add user sections *)
     1.7 -use "../Pure/section_utils.ML";
     1.8 +use "$ISABELLE_HOME/src/Pure/section_utils.ML";
     1.9  use "thy_syntax.ML";
    1.10  
    1.11 -use "../Provers/simplifier.ML";
    1.12 -use "../Provers/splitter.ML";
    1.13 -use "../Provers/hypsubst.ML";
    1.14 -use "../Provers/classical.ML";
    1.15 -use "../Provers/blast.ML";
    1.16 -use "../Provers/nat_transitive.ML";
    1.17 +use "$ISABELLE_HOME/src/Provers/simplifier.ML";
    1.18 +use "$ISABELLE_HOME/src/Provers/splitter.ML";
    1.19 +use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
    1.20 +use "$ISABELLE_HOME/src/Provers/classical.ML";
    1.21 +use "$ISABELLE_HOME/src/Provers/blast.ML";
    1.22 +use "$ISABELLE_HOME/src/Provers/nat_transitive.ML";
    1.23  
    1.24  use "thy_data.ML";
    1.25  
    1.26 @@ -32,7 +32,7 @@
    1.27  
    1.28  use_thy "Ord";
    1.29  use_thy "subset";
    1.30 -use     "typedef.ML";
    1.31 +use "typedef.ML";
    1.32  use_thy "Sum";
    1.33  use_thy "Gfp";
    1.34