src/HOL/Groebner_Basis.thy
 changeset 30240 5b25fee0362c parent 29667 53103fc8ffa3 child 30242 aea5d7fa7ef5
```     1.1 --- a/src/HOL/Groebner_Basis.thy	Wed Mar 04 10:43:39 2009 +0100
1.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Mar 04 10:45:52 2009 +0100
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)
1.12 @@ -436,8 +436,8 @@
1.13  *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
1.14  declare dvd_def[algebra]
1.15  declare dvd_eq_mod_eq_0[symmetric, algebra]
1.16 -declare nat_mod_div_trivial[algebra]
1.17 -declare nat_mod_mod_trivial[algebra]
1.18 +declare mod_div_trivial[algebra]
1.19 +declare mod_mod_trivial[algebra]
1.20  declare conjunct1[OF DIVISION_BY_ZERO, algebra]
1.21  declare conjunct2[OF DIVISION_BY_ZERO, algebra]
1.22  declare zmod_zdiv_equality[symmetric,algebra]
1.23 @@ -448,16 +448,16 @@
1.24  declare zmod_zminus2[algebra]
1.25  declare zdiv_zero[algebra]
1.26  declare zmod_zero[algebra]
1.27 -declare zmod_1[algebra]
1.28 -declare zdiv_1[algebra]
1.29 +declare mod_by_1[algebra]
1.30 +declare div_by_1[algebra]
1.31  declare zmod_minus1_right[algebra]
1.32  declare zdiv_minus1_right[algebra]
1.33  declare mod_div_trivial[algebra]
1.34  declare mod_mod_trivial[algebra]
1.35 -declare zmod_zmult_self1[algebra]
1.36 -declare zmod_zmult_self2[algebra]
1.37 +declare mod_mult_self2_is_0[algebra]
1.38 +declare mod_mult_self1_is_0[algebra]
1.39  declare zmod_eq_0_iff[algebra]
1.40 -declare zdvd_0_left[algebra]
1.41 +declare dvd_0_left_iff[algebra]
1.42  declare zdvd1_eq[algebra]
1.43  declare zmod_eq_dvd_iff[algebra]
1.44  declare nat_mod_eq_iff[algebra]
```