--- a/src/HOL/Presburger.thy Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Presburger.thy Fri Jun 14 08:34:27 2019 +0000
@@ -432,7 +432,7 @@
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 semiring_parity
+context unique_euclidean_semiring_with_nat
begin
declare even_mult_iff [presburger]
@@ -445,7 +445,7 @@
end
-context ring_parity
+context unique_euclidean_ring_with_nat
begin
declare even_minus [presburger]