diff -r c45067867860 -r 54a127873735 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Tue May 22 17:15:02 2018 +0200
+++ b/src/HOL/Rings.thy	Tue May 22 18:14:29 2018 +0000
@@ -137,7 +137,7 @@
 lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
   unfolding dvd_def ..
 
-lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
+lemma dvdE [elim]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
   unfolding dvd_def by blast
 
 end