src/HOL/Number_Theory/UniqueFactorization.thy
changeset 44821 a92f65e174cf
parent 41959 b460124855b8
child 44872 a98ef45122f3
     1.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Sep 07 14:58:40 2011 +0200
     1.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Sep 07 09:02:58 2011 -0700
     1.3 @@ -766,7 +766,7 @@
     1.4  lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
     1.5      \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
     1.6  by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv multiplicity_dvd_int
     1.7 -          multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) zless_le)
     1.8 +          multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) less_le)
     1.9  
    1.10  lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
    1.11      (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"