src/HOL/ROOT.ML
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";