--- a/src/HOL/Tools/lin_arith.ML Fri Jul 27 14:56:37 2012 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri Jul 27 15:42:39 2012 +0200
@@ -811,7 +811,9 @@
@{thm "order_less_irrefl"}, @{thm "zero_neq_one"}, @{thm "zero_less_one"},
@{thm "zero_le_one"}, @{thm "zero_neq_one"} RS not_sym, @{thm "not_one_le_zero"},
@{thm "not_one_less_zero"}]
- addsimprocs [@{simproc abel_cancel_sum}, @{simproc abel_cancel_relation}]
+ addsimprocs [@{simproc group_cancel_add}, @{simproc group_cancel_diff},
+ @{simproc group_cancel_eq}, @{simproc group_cancel_le},
+ @{simproc group_cancel_less}]
(*abel_cancel helps it work in abstract algebraic domains*)
addsimprocs Nat_Arith.nat_cancel_sums_add
|> Simplifier.add_cong @{thm if_weak_cong},