--- a/src/HOL/Number_Theory/UniqueFactorization.thy Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Wed Sep 07 09:02:58 2011 -0700
@@ -766,7 +766,7 @@
lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
\<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv multiplicity_dvd_int
- multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) zless_le)
+ multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) less_le)
lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
(x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"