src/HOL/ROOT.ML
changeset 6260 a8010d459ef7
parent 5983 79e301a6a51b
child 6349 f7750d816c21
     1.1 --- a/src/HOL/ROOT.ML	Mon Feb 08 17:29:08 1999 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Mon Feb 08 17:30:22 1999 +0100
     1.3 @@ -13,21 +13,21 @@
     1.4  print_depth 1;
     1.5  
     1.6  (* Add user sections *)
     1.7 -use "$ISABELLE_HOME/src/Pure/section_utils.ML";
     1.8 +use "~~/src/Pure/section_utils.ML";
     1.9  use "thy_syntax.ML";
    1.10  
    1.11 -use "$ISABELLE_HOME/src/Provers/simplifier.ML";
    1.12 -use "$ISABELLE_HOME/src/Provers/split_paired_all.ML";
    1.13 -use "$ISABELLE_HOME/src/Provers/splitter.ML";
    1.14 -use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
    1.15 -use "$ISABELLE_HOME/src/Provers/classical.ML";
    1.16 -use "$ISABELLE_HOME/src/Provers/blast.ML";
    1.17 -use "$ISABELLE_HOME/src/Provers/clasimp.ML";
    1.18 -use "$ISABELLE_HOME/src/Provers/Arith/fast_lin_arith.ML";
    1.19 -use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML";
    1.20 -use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
    1.21 -use "$ISABELLE_HOME/src/Provers/Arith/abel_cancel.ML";
    1.22 -use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
    1.23 +use "~~/src/Provers/simplifier.ML";
    1.24 +use "~~/src/Provers/split_paired_all.ML";
    1.25 +use "~~/src/Provers/splitter.ML";
    1.26 +use "~~/src/Provers/hypsubst.ML";
    1.27 +use "~~/src/Provers/classical.ML";
    1.28 +use "~~/src/Provers/blast.ML";
    1.29 +use "~~/src/Provers/clasimp.ML";
    1.30 +use "~~/src/Provers/Arith/fast_lin_arith.ML";
    1.31 +use "~~/src/Provers/Arith/cancel_sums.ML";
    1.32 +use "~~/src/Provers/Arith/cancel_factor.ML";
    1.33 +use "~~/src/Provers/Arith/abel_cancel.ML";
    1.34 +use "~~/src/Provers/quantifier1.ML";
    1.35  
    1.36  use_thy "HOL";
    1.37  use "hologic.ML";
    1.38 @@ -60,9 +60,9 @@
    1.39  
    1.40  use_thy "Recdef";
    1.41  (*TFL: recursive function definitions*)
    1.42 -cd "$ISABELLE_HOME/src/TFL";
    1.43 +cd "~~/src/TFL";
    1.44  use "sys.sml";
    1.45 -cd "$ISABELLE_HOME/src/HOL";
    1.46 +cd "~~/src/HOL";
    1.47  
    1.48  cd "Integ";
    1.49  use_thy "IntDef";