tuned prefixes of ac interpretations
authorhaftmann
Thu Mar 11 14:39:58 2010 +0100 (2010-03-11)
changeset 35726059d2f7b979f
parent 35725 4d7e3cc9c52c
child 35727 817b8e0f7086
tuned prefixes of ac interpretations
src/HOL/GCD.thy
src/HOL/Rat.thy
     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)
     2.1 --- a/src/HOL/Rat.thy	Thu Mar 11 14:39:58 2010 +0100
     2.2 +++ b/src/HOL/Rat.thy	Thu Mar 11 14:39:58 2010 +0100
     2.3 @@ -1104,11 +1104,11 @@
     2.4  
     2.5  lemma rat_less_eq_code [code]:
     2.6    "p \<le> q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d \<le> c * b)"
     2.7 -  by (cases p, cases q) (simp add: quotient_of_Fract times.commute)
     2.8 +  by (cases p, cases q) (simp add: quotient_of_Fract mult.commute)
     2.9  
    2.10  lemma rat_less_code [code]:
    2.11    "p < q \<longleftrightarrow> (let (a, c) = quotient_of p; (b, d) = quotient_of q in a * d < c * b)"
    2.12 -  by (cases p, cases q) (simp add: quotient_of_Fract times.commute)
    2.13 +  by (cases p, cases q) (simp add: quotient_of_Fract mult.commute)
    2.14  
    2.15  lemma [code]:
    2.16    "of_rat p = (let (a, b) = quotient_of p in of_int a / of_int b)"