--- a/src/HOL/IntDiv.thy Mon Jun 11 02:25:55 2007 +0200
+++ b/src/HOL/IntDiv.thy Mon Jun 11 05:20:05 2007 +0200
@@ -1327,10 +1327,10 @@
done
lemma zdvd_imp_le: "[| z dvd n; 0 < n |] ==> z \<le> (n::int)"
- apply (rule_tac z=n in int_cases)
- apply (auto simp add: dvd_int_iff)
- apply (rule_tac z=z in int_cases)
- apply (auto simp add: dvd_imp_le)
+ apply (rule_tac z=n in int_cases')
+ apply (auto simp add: dvd_int_of_nat_iff)
+ apply (rule_tac z=z in int_cases')
+ apply (auto simp add: dvd_imp_le)
done