--- a/src/HOL/Int.thy Mon Jul 22 22:55:19 2024 +0100
+++ b/src/HOL/Int.thy Tue Jul 23 15:54:43 2024 +0100
@@ -198,7 +198,7 @@
then have \<open>int n \<ge> int 1\<close>
by (rule of_nat_mono)
with \<open>l - k = int n\<close> show ?Q
- by simp
+ by (simp add: algebra_simps)
qed
qed