consider dvdE for automated classical proving
authorhaftmann
Tue May 22 18:14:29 2018 +0000 (21 months ago)
changeset 6825154a127873735
parent 68250 c45067867860
child 68252 8b284d24f434
consider dvdE for automated classical proving
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Rings.thy	Tue May 22 17:15:02 2018 +0200
     1.2 +++ b/src/HOL/Rings.thy	Tue May 22 18:14:29 2018 +0000
     1.3 @@ -137,7 +137,7 @@
     1.4  lemma dvdI [intro?]: "a = b * k \<Longrightarrow> b dvd a"
     1.5    unfolding dvd_def ..
     1.6  
     1.7 -lemma dvdE [elim?]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
     1.8 +lemma dvdE [elim]: "b dvd a \<Longrightarrow> (\<And>k. a = b * k \<Longrightarrow> P) \<Longrightarrow> P"
     1.9    unfolding dvd_def by blast
    1.10  
    1.11  end