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>\fast_nat_arith_simproc\ anyway. However, it seems cheaper to activate the solver all the time rather than add the additional check.\ -lemmas [arith_split] = nat_diff_split split_min split_max +lemmas [linarith_split] = nat_diff_split split_min split_max text\Lemmas \divide_simps\ move division to the outside and eliminates them on (in)equalities.\