1.1 --- a/src/HOL/Groebner_Basis.thy	Thu Feb 18 13:29:59 2010 -0800
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Thu Feb 18 14:21:44 2010 -0800
     1.3 @@ -143,16 +143,16 @@
     1.4  next show "mul (pwr x p) (pwr x q) = pwr x (p + q)" by (rule mul_pwr)
     1.5  next show "mul x (pwr x q) = pwr x (Suc q)" using pwr_Suc by simp
     1.6  next show "mul (pwr x q) x = pwr x (Suc q)" using pwr_Suc mul_c by simp
     1.7 -next show "mul x x = pwr x 2" by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
     1.8 +next show "mul x x = pwr x 2" by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c)
     1.9  next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul)
    1.10  next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr)
    1.11  next show "pwr x 0 = r1" using pwr_0 .
    1.12 -next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
    1.13 +next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c)
    1.14  next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp
    1.15  next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp
    1.16 -next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number mul_pwr)
    1.17 +next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number' mul_pwr)
    1.18  next show "pwr x (Suc (2 * n)) = mul x (mul (pwr x n) (pwr x n))"
    1.19 -    by (simp add: nat_number pwr_Suc mul_pwr)
    1.20 +    by (simp add: nat_number' pwr_Suc mul_pwr)
    1.21  qed
    1.22  
    1.23  
    1.24 @@ -165,7 +165,7 @@
    1.25  
    1.26  interpretation class_semiring: gb_semiring
    1.27      "op +" "op *" "op ^" "0::'a::{comm_semiring_1}" "1"
    1.28 -  proof qed (auto simp add: algebra_simps power_Suc)
    1.29 +  proof qed (auto simp add: algebra_simps)
    1.30  
    1.31  lemmas nat_arith =
    1.32    add_nat_number_of
    1.33 @@ -175,7 +175,7 @@
    1.34    less_nat_number_of
    1.35  
    1.36  lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
    1.37 -  by (simp add: numeral_1_eq_1)
    1.38 +  by simp
    1.39  
    1.40  lemmas comp_arith =
    1.41    Let_def arith_simps nat_arith rel_simps neg_simps if_False
    1.42 @@ -350,7 +350,7 @@
    1.43  
    1.44  interpretation class_ringb: ringb
    1.45    "op +" "op *" "op ^" "0::'a::{idom,number_ring}" "1" "op -" "uminus"
    1.46 -proof(unfold_locales, simp add: algebra_simps power_Suc, auto)
    1.47 +proof(unfold_locales, simp add: algebra_simps, auto)
    1.48    fix w x y z ::"'a::{idom,number_ring}"
    1.49    assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    1.50    hence ynz': "y - z \<noteq> 0" by simp
    1.51 @@ -366,7 +366,7 @@
    1.52  
    1.53  interpretation natgb: semiringb
    1.54    "op +" "op *" "op ^" "0::nat" "1"
    1.55 -proof (unfold_locales, simp add: algebra_simps power_Suc)
    1.56 +proof (unfold_locales, simp add: algebra_simps)
    1.57    fix w x y z ::"nat"
    1.58    { assume p: "w * y + x * z = w * z + x * y" and ynz: "y \<noteq> z"
    1.59      hence "y < z \<or> y > z" by arith
    1.60 @@ -375,13 +375,13 @@
    1.61        then obtain k where kp: "k>0" and yz:"z = y + k" by blast
    1.62        from p have "(w * y + x *y) + x*k = (w * y + x*y) + w*k" by (simp add: yz algebra_simps)
    1.63        hence "x*k = w*k" by simp
    1.64 -      hence "w = x" using kp by (simp add: mult_cancel2) }
    1.65 +      hence "w = x" using kp by simp }
    1.66      moreover {
    1.67        assume lt: "y >z" hence "\<exists>k. y = z + k \<and> k>0" by (rule_tac x="y - z" in exI, auto)
    1.68        then obtain k where kp: "k>0" and yz:"y = z + k" by blast
    1.69        from p have "(w * z + x *z) + w*k = (w * z + x*z) + x*k" by (simp add: yz algebra_simps)
    1.70        hence "w*k = x*k" by simp
    1.71 -      hence "w = x" using kp by (simp add: mult_cancel2)}
    1.72 +      hence "w = x" using kp by simp }
    1.73      ultimately have "w=x" by blast }
    1.74    thus "(w * y + x * z = w * z + x * y) = (w = x \<or> y = z)" by auto
    1.75  qed