changeset 14398 | c5c47703f763 |
parent 14387 | e96d5c42c4b0 |
child 15103 | 79846e8792eb |
--- a/src/HOL/ROOT.ML Thu Feb 19 10:41:32 2004 +0100 +++ b/src/HOL/ROOT.ML Thu Feb 19 15:57:34 2004 +0100 @@ -34,7 +34,7 @@ use "~~/src/Provers/Arith/cancel_numeral_factor.ML"; use "~~/src/Provers/Arith/extract_common_term.ML"; use "~~/src/Provers/Arith/cancel_div_mod.ML"; -use "~~/src/Provers/linorder.ML"; +use "~~/src/Provers/order.ML"; with_path "Integ" use_thy "Main";