# HG changeset patch
# User haftmann
# Date 1268314798 -3600
# Node ID 059d2f7b979f2fc396fd08dc0a7eb2dbfc824c56
# Parent  4d7e3cc9c52c8a723bdea327fcde1269eb86de94
tuned prefixes of ac interpretations

diff -r 4d7e3cc9c52c -r 059d2f7b979f src/HOL/GCD.thy
--- 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)
diff -r 4d7e3cc9c52c -r 059d2f7b979f src/HOL/Rat.thy
--- 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)"