src/HOL/Groebner_Basis.thy
changeset 30079 293b896b9c25
parent 30042 31039ee583fa
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Groebner_Basis.thy	Mon Feb 23 13:55:36 2009 -0800
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Feb 23 16:25:52 2009 -0800
     1.3 @@ -147,7 +147,7 @@
     1.4  next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul)
     1.5  next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr)
     1.6  next show "pwr x 0 = r1" using pwr_0 .
     1.7 -next show "pwr x 1 = x" by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
     1.8 +next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number pwr_Suc pwr_0 mul_1 mul_c)
     1.9  next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp
    1.10  next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp
    1.11  next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number mul_pwr)