src/HOL/GCD.thy
changeset 44766 d4d33a4d7548
parent 44278 1220ecb81e8f
child 44821 a92f65e174cf
     1.1 --- a/src/HOL/GCD.thy	Tue Sep 06 16:30:39 2011 -0700
     1.2 +++ b/src/HOL/GCD.thy	Tue Sep 06 19:03:41 2011 -0700
     1.3 @@ -1452,7 +1452,7 @@
     1.4  by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat)
     1.5  
     1.6  lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
     1.7 -by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le)
     1.8 +by (metis lcm_0_int lcm_0_left_int lcm_pos_int less_le)
     1.9  
    1.10  lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
    1.11  by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat)