Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Number_Theory/Eratosthenes.thy
changeset 82774 2865a6618cba
parent 80914 d97fdabd9e2b 
--- a/src/HOL/Number_Theory/Eratosthenes.thy	Thu Jun 26 17:25:29 2025 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Thu Jun 26 17:25:29 2025 +0200
@@ -223,7 +223,7 @@
     from 1 have *: "\<And>q. Suc n < q \<Longrightarrow> q \<le> Suc (n + length bs) \<Longrightarrow>
       bs ! (q - Suc (Suc n)) \<Longrightarrow> \<not> Suc n dvd q \<Longrightarrow> q dvd m \<Longrightarrow> m dvd q"
       by auto
-    from 2 have "\<not> Suc n dvd q" by (auto elim: dvdE)
+    from 2 have "\<not> Suc n dvd q" by auto
     moreover note 3
     moreover note \<open>q dvd m\<close>
     ultimately show ?thesis by (auto intro: *)
isabelle