1.1 --- a/src/HOL/Groebner_Basis.thy	Tue Mar 27 12:42:54 2012 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Tue Mar 27 14:49:56 2012 +0200
     1.3 @@ -50,16 +50,16 @@
     1.4  declare dvd_eq_mod_eq_0[symmetric, algebra]
     1.5  declare mod_div_trivial[algebra]
     1.6  declare mod_mod_trivial[algebra]
     1.7 -declare conjunct1[OF DIVISION_BY_ZERO, algebra]
     1.8 -declare conjunct2[OF DIVISION_BY_ZERO, algebra]
     1.9 +declare div_by_0[algebra]
    1.10 +declare mod_by_0[algebra]
    1.11  declare zmod_zdiv_equality[symmetric,algebra]
    1.12  declare zdiv_zmod_equality[symmetric, algebra]
    1.13  declare zdiv_zminus_zminus[algebra]
    1.14  declare zmod_zminus_zminus[algebra]
    1.15  declare zdiv_zminus2[algebra]
    1.16  declare zmod_zminus2[algebra]
    1.17 -declare zdiv_zero[algebra]
    1.18 -declare zmod_zero[algebra]
    1.19 +declare div_0[algebra]
    1.20 +declare mod_0[algebra]
    1.21  declare mod_by_1[algebra]
    1.22  declare div_by_1[algebra]
    1.23  declare zmod_minus1_right[algebra]