diff -r b9e54ba563b3 -r 1436d81d1294 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Sun Jul 20 23:07:03 2008 +0200
+++ b/src/HOL/Groebner_Basis.thy	Mon Jul 21 13:36:39 2008 +0200
@@ -13,7 +13,6 @@
   ("Tools/Groebner_Basis/groebner.ML")
 begin
 
-
 subsection {* Semiring normalization *}
 
 setup NormalizerData.setup
@@ -251,6 +250,7 @@
 
 use "Tools/Groebner_Basis/normalizer.ML"
 
+
 method_setup sring_norm = {*
   Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD' (Normalizer.semiring_normalize_tac ctxt))
 *} "semiring normalizer"
@@ -415,7 +415,6 @@
     "P \<equiv> False \<Longrightarrow> \<not> P"
     "\<not> P \<Longrightarrow> (P \<equiv> False)"
   by auto
-
 use "Tools/Groebner_Basis/groebner.ML"
 
 method_setup algebra =
@@ -434,5 +433,32 @@
        Method.SIMPLE_METHOD' (Groebner.algebra_tac add_ths del_ths ctxt))
 end
 *} "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 conjunct1[OF DIVISION_BY_ZERO, algebra]
+declare conjunct2[OF DIVISION_BY_ZERO, algebra]
+declare zmod_zdiv_equality[symmetric,algebra]
+declare zdiv_zmod_equality[symmetric, algebra]
+declare zdiv_zminus_zminus[algebra]
+declare zmod_zminus_zminus[algebra]
+declare zdiv_zminus2[algebra]
+declare zmod_zminus2[algebra]
+declare zdiv_zero[algebra]
+declare zmod_zero[algebra]
+declare zmod_1[algebra]
+declare zdiv_1[algebra]
+declare zmod_minus1_right[algebra]
+declare zdiv_minus1_right[algebra]
+declare mod_div_trivial[algebra]
+declare mod_mod_trivial[algebra]
+declare zmod_zmult_self1[algebra]
+declare zmod_zmult_self2[algebra]
+declare zmod_eq_0_iff[algebra]
+declare zdvd_0_left[algebra]
+declare zdvd1_eq[algebra]
+declare zmod_eq_dvd_iff[algebra]
+declare nat_mod_eq_iff[algebra]
 
 end