| changeset 10535 | c00b1d0d46ac |
| parent 10275 | 558f7569026e |
| child 10689 | 5c44de6aadf4 |
--- a/src/HOL/ROOT.ML Tue Nov 28 16:21:51 2000 +0100 +++ b/src/HOL/ROOT.ML Wed Nov 29 10:19:32 2000 +0100 @@ -33,6 +33,7 @@ use "~~/src/Provers/quantifier1.ML"; use "~~/src/Provers/Arith/cancel_numerals.ML"; use "~~/src/Provers/Arith/combine_numerals.ML"; +use "~~/src/Provers/Arith/cancel_numeral_factor.ML"; with_path "Integ" use_thy "Main";