changeset 26101 | a657683e902a |
parent 26061 | 59de52bec3ec |
child 26110 | 06eacfd8dd9f |
--- a/src/HOL/Tools/lin_arith.ML Wed Feb 20 14:52:34 2008 +0100 +++ b/src/HOL/Tools/lin_arith.ML Wed Feb 20 14:52:38 2008 +0100 @@ -810,7 +810,7 @@ @{thm "not_one_less_zero"}] addsimprocs [ab_group_add_cancel.sum_conv, ab_group_add_cancel.rel_conv] (*abel_cancel helps it work in abstract algebraic domains*) - addsimprocs nat_cancel_sums_add}) #> + addsimprocs ArithData.nat_cancel_sums_add}) #> arith_discrete "nat"; val lin_arith_simproc = Fast_Arith.lin_arith_simproc;