
diff -r dc758531077b -r fcd118d9242f src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Fri Aug 19 05:49:07 2022 +0000
+++ b/src/HOL/Fields.thy	Fri Aug 19 05:49:09 2022 +0000
@@ -85,7 +85,7 @@
    \<^text>\<open>fast_nat_arith_simproc\<close> anyway. However, it seems cheaper to activate the
    solver all the time rather than add the additional check.\<close>
 
-lemmas [arith_split] = nat_diff_split split_min split_max
+lemmas [linarith_split] = nat_diff_split split_min split_max
 
 text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close>
 




