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.
consider dvdE for automated classical proving
authorhaftmann
Tue, 22 May 2018 18:14:29 +0000
changeset 68251 54a127873735
parent 68250 c45067867860
child 68252 8b284d24f434
consider dvdE for automated classical proving
src/HOL/Rings.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle