1.1 --- a/src/HOL/ROOT.ML	Fri Jul 23 16:54:28 1999 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Fri Jul 23 17:24:48 1999 +0200
     1.3 @@ -27,10 +27,12 @@
     1.4  use "~~/src/Provers/Arith/cancel_sums.ML";
     1.5  use "~~/src/Provers/Arith/cancel_factor.ML";
     1.6  use "~~/src/Provers/Arith/abel_cancel.ML";
     1.7 +use "~~/src/Provers/Arith/assoc_fold.ML";
     1.8  use "~~/src/Provers/quantifier1.ML";
     1.9  
    1.10  use_thy "HOL";
    1.11  use "hologic.ML";
    1.12 +use "~~/src/Provers/Arith/combine_coeff.ML";
    1.13  use "cladata.ML";
    1.14  use "simpdata.ML";
    1.15  
    1.16 @@ -70,6 +72,7 @@
    1.17  use_thy "IntDef";
    1.18  use "simproc.ML";
    1.19  use_thy "NatBin";
    1.20 +use "bin_simprocs.ML";
    1.21  cd "..";
    1.22  
    1.23  (*the all-in-one theory*)