# HG changeset patch
# User wenzelm
# Date 1752152906 -7200
# Node ID cd566dbe9f48eb159ae4efb28e9b5d33d38352cb
# Parent  68a0219861b7964b05984086b68b2c6366c95bcb
tuned proof;

diff -r 68a0219861b7 -r cd566dbe9f48 src/ZF/IntDiv.thy
--- a/src/ZF/IntDiv.thy	Thu Jul 10 12:40:45 2025 +0200
+++ b/src/ZF/IntDiv.thy	Thu Jul 10 15:08:26 2025 +0200
@@ -304,8 +304,7 @@
 apply (auto simp add: not_zless_iff_zle
                       not_zle_iff_zless [THEN iff_sym, of "m$*k"]
                       not_zle_iff_zless [THEN iff_sym, of m])
-apply (auto elim: notE
-            simp add: zless_imp_zle zmult_zle_mono1 zmult_zle_mono1_neg)
+apply (auto simp add: zless_imp_zle zmult_zle_mono1 zmult_zle_mono1_neg)
 done
 
 lemma zmult_zless_cancel2: