| changeset 68251 | 54a127873735 |
| parent 67689 | 2c38ffd6ec71 |
| child 68252 | 8b284d24f434 |
--- 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