src/HOL/Groebner_Basis.thy
changeset 30027 ab40c5e007e0
parent 29667 53103fc8ffa3
child 30031 bd786c37af84
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Feb 20 16:48:17 2009 +0100
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Feb 20 20:50:49 2009 +0100
     1.3 @@ -436,8 +436,8 @@
     1.4  *} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
     1.5  declare dvd_def[algebra]
     1.6  declare dvd_eq_mod_eq_0[symmetric, algebra]
     1.7 -declare nat_mod_div_trivial[algebra]
     1.8 -declare nat_mod_mod_trivial[algebra]
     1.9 +declare mod_div_trivial[algebra]
    1.10 +declare mod_mod_trivial[algebra]
    1.11  declare conjunct1[OF DIVISION_BY_ZERO, algebra]
    1.12  declare conjunct2[OF DIVISION_BY_ZERO, algebra]
    1.13  declare zmod_zdiv_equality[symmetric,algebra]