src/HOL/IntDiv.thy
changeset 31662 57f7ef0dba8e
parent 31068 f591144b0f17
child 31734 a4a79836d07b
     1.1 --- a/src/HOL/IntDiv.thy	Mon Jun 15 17:59:36 2009 -0700
     1.2 +++ b/src/HOL/IntDiv.thy	Mon Jun 15 21:29:04 2009 -0700
     1.3 @@ -1059,13 +1059,10 @@
     1.4  done
     1.5  
     1.6  lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
     1.7 -  by (auto elim!: dvdE simp add: mod_mult_mult1)
     1.8 +  by (rule dvd_mod) (* TODO: remove *)
     1.9  
    1.10  lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
    1.11 -  apply (subgoal_tac "k dvd n * (m div n) + m mod n")
    1.12 -   apply (simp add: zmod_zdiv_equality [symmetric])
    1.13 -  apply (simp only: dvd_add dvd_mult2)
    1.14 -  done
    1.15 +  by (rule dvd_mod_imp_dvd) (* TODO: remove *)
    1.16  
    1.17  lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
    1.18    apply (auto elim!: dvdE)