src/HOL/ROOT.ML
changeset 5983 79e301a6a51b
parent 5699 5b9a359e083c
child 6260 a8010d459ef7
     1.1 --- a/src/HOL/ROOT.ML	Fri Nov 27 16:54:59 1998 +0100
     1.2 +++ b/src/HOL/ROOT.ML	Fri Nov 27 17:00:30 1998 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  use "$ISABELLE_HOME/src/Provers/classical.ML";
     1.5  use "$ISABELLE_HOME/src/Provers/blast.ML";
     1.6  use "$ISABELLE_HOME/src/Provers/clasimp.ML";
     1.7 -use "$ISABELLE_HOME/src/Provers/Arith/nat_transitive.ML";
     1.8 +use "$ISABELLE_HOME/src/Provers/Arith/fast_lin_arith.ML";
     1.9  use "$ISABELLE_HOME/src/Provers/Arith/cancel_sums.ML";
    1.10  use "$ISABELLE_HOME/src/Provers/Arith/cancel_factor.ML";
    1.11  use "$ISABELLE_HOME/src/Provers/Arith/abel_cancel.ML";
    1.12 @@ -57,7 +57,6 @@
    1.13  use_thy "Record";
    1.14  
    1.15  use_thy "Arith";
    1.16 -use "arith_data.ML";
    1.17  
    1.18  use_thy "Recdef";
    1.19  (*TFL: recursive function definitions*)