--- a/src/HOL/Groebner_Basis.thy Fri Feb 20 16:48:17 2009 +0100
+++ b/src/HOL/Groebner_Basis.thy Fri Feb 20 20:50:49 2009 +0100
@@ -436,8 +436,8 @@
*} "solve polynomial equations over (semi)rings and ideal membership problems using Groebner bases"
declare dvd_def[algebra]
declare dvd_eq_mod_eq_0[symmetric, algebra]
-declare nat_mod_div_trivial[algebra]
-declare nat_mod_mod_trivial[algebra]
+declare mod_div_trivial[algebra]
+declare mod_mod_trivial[algebra]
declare conjunct1[OF DIVISION_BY_ZERO, algebra]
declare conjunct2[OF DIVISION_BY_ZERO, algebra]
declare zmod_zdiv_equality[symmetric,algebra]