--- a/src/HOL/GCD.thy Thu Mar 11 14:39:58 2010 +0100
+++ b/src/HOL/GCD.thy Thu Mar 11 14:39:58 2010 +0100
@@ -1358,10 +1358,10 @@
done
lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
- using lcm_dvd1_nat [of n m] by (simp only: lcm_nat_def times.commute gcd_nat.commute)
+ using lcm_dvd1_nat [of n m] by (simp only: lcm_nat_def mult.commute gcd_nat.commute)
lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
- using lcm_dvd1_int [of n m] by (simp only: lcm_int_def lcm_nat_def times.commute gcd_nat.commute)
+ using lcm_dvd1_int [of n m] by (simp only: lcm_int_def lcm_nat_def mult.commute gcd_nat.commute)
lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
by(metis lcm_dvd1_nat dvd_trans)
--- a/src/HOL/Rat.thy Thu Mar 11 14:39:58 2010 +0100
+++ b/src/HOL/Rat.thy Thu Mar 11 14:39:58 2010 +0100
@@ -1104,11 +1104,11 @@
lemma rat_less_eq_code [code]:
"p \<le> q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d \<le> c * b)"
- by (cases p, cases q) (simp add: quotient_of_Fract times.commute)
+ by (cases p, cases q) (simp add: quotient_of_Fract mult.commute)
lemma rat_less_code [code]:
"p < q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d < c * b)"
- by (cases p, cases q) (simp add: quotient_of_Fract times.commute)
+ by (cases p, cases q) (simp add: quotient_of_Fract mult.commute)
lemma [code]:
"of_rat p = (let (a, b) = quotient_of p in of_int a / of_int b)"