src/HOL/GCD.thy
changeset 36350 bc7982c54e37
parent 35726 059d2f7b979f
child 37770 cddb3106adb8
     1.1 --- a/src/HOL/GCD.thy	Mon Apr 26 11:34:17 2010 +0200
     1.2 +++ b/src/HOL/GCD.thy	Mon Apr 26 11:34:19 2010 +0200
     1.3 @@ -1034,11 +1034,11 @@
     1.4      thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
     1.5        apply (simp add: bezw_non_0 gcd_non_0_nat)
     1.6        apply (erule subst)
     1.7 -      apply (simp add: ring_simps)
     1.8 +      apply (simp add: field_simps)
     1.9        apply (subst mod_div_equality [of m n, symmetric])
    1.10        (* applying simp here undoes the last substitution!
    1.11           what is procedure cancel_div_mod? *)
    1.12 -      apply (simp only: ring_simps zadd_int [symmetric]
    1.13 +      apply (simp only: field_simps zadd_int [symmetric]
    1.14          zmult_int [symmetric])
    1.15        done
    1.16  qed
    1.17 @@ -1389,7 +1389,7 @@
    1.18    show "lcm (lcm n m) p = lcm n (lcm m p)"
    1.19      by (rule lcm_unique_nat [THEN iffD1]) (metis dvd.order_trans lcm_unique_nat)
    1.20    show "lcm m n = lcm n m"
    1.21 -    by (simp add: lcm_nat_def gcd_commute_nat ring_simps)
    1.22 +    by (simp add: lcm_nat_def gcd_commute_nat field_simps)
    1.23  qed
    1.24  
    1.25  interpretation lcm_int!: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"