src/HOL/IntDiv.thy
changeset 23307 2fe3345035c7
parent 23306 cdb027d0637e
child 23365 f31794033ae1
     1.1 --- a/src/HOL/IntDiv.thy	Mon Jun 11 02:25:55 2007 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Mon Jun 11 05:20:05 2007 +0200
     1.3 @@ -1327,10 +1327,10 @@
     1.4    done
     1.5  
     1.6  lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
     1.7 -  apply (rule_tac z=n in int_cases)
     1.8 -  apply (auto simp add: dvd_int_iff) 
     1.9 -  apply (rule_tac z=z in int_cases) 
    1.10 -  apply (auto simp add: dvd_imp_le) 
    1.11 +  apply (rule_tac z=n in int_cases')
    1.12 +  apply (auto simp add: dvd_int_of_nat_iff)
    1.13 +  apply (rule_tac z=z in int_cases')
    1.14 +  apply (auto simp add: dvd_imp_le)
    1.15    done
    1.16  
    1.17