src/HOL/GCD.thy
changeset 35726 059d2f7b979f
parent 35644 d20cf282342e
child 36350 bc7982c54e37
     1.1 --- a/src/HOL/GCD.thy	Thu Mar 11 14:39:58 2010 +0100
     1.2 +++ b/src/HOL/GCD.thy	Thu Mar 11 14:39:58 2010 +0100
     1.3 @@ -1358,10 +1358,10 @@
     1.4  done
     1.5  
     1.6  lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
     1.7 -  using lcm_dvd1_nat [of n m] by (simp only: lcm_nat_def times.commute gcd_nat.commute)
     1.8 +  using lcm_dvd1_nat [of n m] by (simp only: lcm_nat_def mult.commute gcd_nat.commute)
     1.9  
    1.10  lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
    1.11 -  using lcm_dvd1_int [of n m] by (simp only: lcm_int_def lcm_nat_def times.commute gcd_nat.commute)
    1.12 +  using lcm_dvd1_int [of n m] by (simp only: lcm_int_def lcm_nat_def mult.commute gcd_nat.commute)
    1.13  
    1.14  lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
    1.15  by(metis lcm_dvd1_nat dvd_trans)