~~;
authorwenzelm
Mon Feb 08 17:30:22 1999 +0100 (1999-02-08)
changeset 6260a8010d459ef7
parent 6259 488bdc1bd11a
child 6261 6dc692fb3d28
~~;
src/CTT/ROOT.ML
src/FOL/ROOT.ML
src/HOL/ROOT.ML
src/ZF/ROOT.ML
     1.1 --- a/src/CTT/ROOT.ML	Mon Feb 08 17:29:08 1999 +0100
     1.2 +++ b/src/CTT/ROOT.ML	Mon Feb 08 17:30:22 1999 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  print_depth 1;  
     1.5  
     1.6  use_thy "CTT";
     1.7 -use "$ISABELLE_HOME/src/Provers/typedsimp.ML";
     1.8 +use "~~/src/Provers/typedsimp.ML";
     1.9  use "rew.ML";
    1.10  use_thy "Arith";
    1.11  use_thy "Bool";
     2.1 --- a/src/FOL/ROOT.ML	Mon Feb 08 17:29:08 1999 +0100
     2.2 +++ b/src/FOL/ROOT.ML	Mon Feb 08 17:30:22 1999 +0100
     2.3 @@ -13,14 +13,14 @@
     2.4  
     2.5  print_depth 1;  
     2.6  
     2.7 -use "$ISABELLE_HOME/src/Provers/simplifier.ML";
     2.8 -use "$ISABELLE_HOME/src/Provers/splitter.ML";
     2.9 -use "$ISABELLE_HOME/src/Provers/ind.ML";
    2.10 -use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
    2.11 -use "$ISABELLE_HOME/src/Provers/classical.ML";
    2.12 -use "$ISABELLE_HOME/src/Provers/blast.ML";
    2.13 -use "$ISABELLE_HOME/src/Provers/clasimp.ML";
    2.14 -use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
    2.15 +use "~~/src/Provers/simplifier.ML";
    2.16 +use "~~/src/Provers/splitter.ML";
    2.17 +use "~~/src/Provers/ind.ML";
    2.18 +use "~~/src/Provers/hypsubst.ML";
    2.19 +use "~~/src/Provers/classical.ML";
    2.20 +use "~~/src/Provers/blast.ML";
    2.21 +use "~~/src/Provers/clasimp.ML";
    2.22 +use "~~/src/Provers/quantifier1.ML";
    2.23  
    2.24  use_thy "IFOL";
    2.25  use "fologic.ML";
     3.1 --- a/src/HOL/ROOT.ML	Mon Feb 08 17:29:08 1999 +0100
     3.2 +++ b/src/HOL/ROOT.ML	Mon Feb 08 17:30:22 1999 +0100
     3.3 @@ -13,21 +13,21 @@
     3.4  print_depth 1;
     3.5  
     3.6  (* Add user sections *)
     3.7 -use "$ISABELLE_HOME/src/Pure/section_utils.ML";
     3.8 +use "~~/src/Pure/section_utils.ML";
     3.9  use "thy_syntax.ML";
    3.10  
    3.11 -use "$ISABELLE_HOME/src/Provers/simplifier.ML";
    3.12 -use "$ISABELLE_HOME/src/Provers/split_paired_all.ML";
    3.13 -use "$ISABELLE_HOME/src/Provers/splitter.ML";
    3.14 -use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
    3.15 -use "$ISABELLE_HOME/src/Provers/classical.ML";
    3.16 -use "$ISABELLE_HOME/src/Provers/blast.ML";
    3.17 -use "$ISABELLE_HOME/src/Provers/clasimp.ML";
    3.18 -use "$ISABELLE_HOME/src/Provers/Arith/fast_lin_arith.ML";
    3.19 -use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML";
    3.20 -use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
    3.21 -use "$ISABELLE_HOME/src/Provers/Arith/abel_cancel.ML";
    3.22 -use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
    3.23 +use "~~/src/Provers/simplifier.ML";
    3.24 +use "~~/src/Provers/split_paired_all.ML";
    3.25 +use "~~/src/Provers/splitter.ML";
    3.26 +use "~~/src/Provers/hypsubst.ML";
    3.27 +use "~~/src/Provers/classical.ML";
    3.28 +use "~~/src/Provers/blast.ML";
    3.29 +use "~~/src/Provers/clasimp.ML";
    3.30 +use "~~/src/Provers/Arith/fast_lin_arith.ML";
    3.31 +use "~~/src/Provers/Arith/cancel_sums.ML";
    3.32 +use "~~/src/Provers/Arith/cancel_factor.ML";
    3.33 +use "~~/src/Provers/Arith/abel_cancel.ML";
    3.34 +use "~~/src/Provers/quantifier1.ML";
    3.35  
    3.36  use_thy "HOL";
    3.37  use "hologic.ML";
    3.38 @@ -60,9 +60,9 @@
    3.39  
    3.40  use_thy "Recdef";
    3.41  (*TFL: recursive function definitions*)
    3.42 -cd "$ISABELLE_HOME/src/TFL";
    3.43 +cd "~~/src/TFL";
    3.44  use "sys.sml";
    3.45 -cd "$ISABELLE_HOME/src/HOL";
    3.46 +cd "~~/src/HOL";
    3.47  
    3.48  cd "Integ";
    3.49  use_thy "IntDef";
     4.1 --- a/src/ZF/ROOT.ML	Mon Feb 08 17:29:08 1999 +0100
     4.2 +++ b/src/ZF/ROOT.ML	Mon Feb 08 17:30:22 1999 +0100
     4.3 @@ -16,7 +16,7 @@
     4.4  print_depth 1;
     4.5  
     4.6  (*Add user sections for inductive/datatype definitions*)
     4.7 -use     "$ISABELLE_HOME/src/Pure/section_utils";
     4.8 +use     "~~/src/Pure/section_utils";
     4.9  use     "thy_syntax";
    4.10  
    4.11  use_thy "Let";