changeset 8736 | 0bfd6678a5fa |
parent 7739 | bfe45b716dfc |
child 8757 | 04d01ae28508 |
--- a/src/HOL/ROOT.ML Tue Apr 18 14:57:18 2000 +0200 +++ b/src/HOL/ROOT.ML Tue Apr 18 15:51:59 2000 +0200 @@ -31,6 +31,9 @@ use "~~/src/Provers/Arith/assoc_fold.ML"; use "~~/src/Provers/quantifier1.ML"; use "~~/src/Provers/Arith/combine_coeff.ML"; +use "~~/src/Provers/Arith/inverse_fold.ML"; +use "~~/src/Provers/Arith/cancel_numerals.ML"; +use "~~/src/Provers/Arith/fold_Suc.ML"; with_path "Integ" use_thy "Main";