src/HOL/Tools/lin_arith.ML

         @{thm add_0_right},
         @{thm "Zero_not_Suc"}, @{thm "Suc_not_Zero"}, @{thm "le_0_eq"}, @{thm "One_nat_def"},
         @{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},
     number_of = number_of}) #>
   add_discrete_type @{type_name nat};