--- a/src/HOL/Groebner_Basis.thy Fri Oct 24 15:07:51 2014 +0200
+++ b/src/HOL/Groebner_Basis.thy Thu Oct 23 19:40:39 2014 +0200
@@ -5,7 +5,7 @@
header {* Groebner bases *}
theory Groebner_Basis
-imports Semiring_Normalization
+imports Semiring_Normalization Parity
keywords "try0" :: diag
begin
@@ -77,4 +77,22 @@
declare zmod_eq_dvd_iff[algebra]
declare nat_mod_eq_iff[algebra]
+context semiring_parity
+begin
+
+declare even_times_iff [algebra]
+declare even_power [algebra]
+
end
+
+context ring_parity
+begin
+
+declare even_minus [algebra]
+
+end
+
+declare even_Suc [algebra]
+declare even_diff_nat [algebra]
+
+end