changeset 13517 | 42efec18f5b2 |
parent 13403 | bc2b32ee62fd |
child 13735 | 7de9342aca7a |
--- a/src/HOL/ROOT.ML Fri Aug 23 07:34:20 2002 +0200 +++ b/src/HOL/ROOT.ML Fri Aug 23 07:41:05 2002 +0200 @@ -34,6 +34,7 @@ use "~~/src/Provers/Arith/combine_numerals.ML"; use "~~/src/Provers/Arith/cancel_numeral_factor.ML"; use "~~/src/Provers/Arith/extract_common_term.ML"; +use "~~/src/Provers/Arith/cancel_div_mod.ML"; with_path "Integ" use_thy "Main";