changeset 73535 | 0f33c7031ec9 |
parent 72610 | 00fce84413db |
child 74101 | d804e93ae9ff |
--- a/src/HOL/Divides.thy Mon Apr 05 22:46:41 2021 +0200 +++ b/src/HOL/Divides.thy Tue Apr 06 18:12:20 2021 +0000 @@ -147,7 +147,7 @@ proof (cases "sgn l = sgn k") case True then show ?thesis - by (simp add: div_eq_sgn_abs) + by (auto simp add: div_eq_sgn_abs) next case False with \<open>k \<noteq> 0\<close> \<open>l \<noteq> 0\<close>