--- a/src/HOL/Numeral_Simprocs.thy Fri Aug 19 05:49:07 2022 +0000
+++ b/src/HOL/Numeral_Simprocs.thy Fri Aug 19 05:49:09 2022 +0000
@@ -20,8 +20,8 @@
numeral_One [symmetric] uminus_numeral_One [symmetric] Suc_eq_plus1
eq_numeral_iff_iszero not_iszero_Numeral1
-declare split_div [of _ _ "numeral k", arith_split] for k
-declare split_mod [of _ _ "numeral k", arith_split] for k
+declare split_div [of _ _ "numeral k", linarith_split] for k
+declare split_mod [of _ _ "numeral k", linarith_split] for k
text \<open>For \<open>combine_numerals\<close>\<close>