src/HOL/Groebner_Basis.thy
changeset 30034 60f64f112174
parent 30031 bd786c37af84
child 30042 31039ee583fa
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Feb 20 23:46:03 2009 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sat Feb 21 09:58:26 2009 +0100
     1.3 @@ -454,8 +454,8 @@
     1.4  declare zdiv_minus1_right[algebra]
     1.5  declare mod_div_trivial[algebra]
     1.6  declare mod_mod_trivial[algebra]
     1.7 -declare zmod_zmult_self1[algebra]
     1.8 -declare zmod_zmult_self2[algebra]
     1.9 +declare mod_mult_self2_is_0[algebra]
    1.10 +declare mod_mult_self1_is_0[algebra]
    1.11  declare zmod_eq_0_iff[algebra]
    1.12  declare zdvd_0_left[algebra]
    1.13  declare zdvd1_eq[algebra]