Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned proof;
authorwenzelm
Thu, 10 Jul 2025 15:08:26 +0200
changeset 82837 cd566dbe9f48
parent 82836 68a0219861b7
child 82838 ca600cbfd4bf
tuned proof;
src/ZF/IntDiv.thy file | annotate | diff | comparison | revisions 
--- 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:
isabelle