src/HOL/Presburger.thy

 lemma [presburger, algebra]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
 lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
 lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
 lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
 
-context unique_euclidean_semiring_with_nat
+context semiring_parity
 begin
 
 declare even_mult_iff [presburger]
 
 declare even_power [presburger]

   "even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b"
   by auto
 
 end
 
-context unique_euclidean_ring_with_nat
+context ring_parity
 begin
 
 declare even_minus [presburger]
 
 end