--- a/src/HOL/Number_Theory/Cong.thy Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Number_Theory/Cong.thy Wed Oct 09 23:38:29 2024 +0200
@@ -37,11 +37,13 @@
context unique_euclidean_semiring
begin
-definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(1[_ = _] '(' mod _'))\<close>)
- where "cong b c a \<longleftrightarrow> b mod a = c mod a"
+definition cong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ (\<open>(\<open>indent=1 notation=\<open>mixfix cong\<close>\<close>[_ = _] '(' mod _'))\<close>)
+ where "[b = c] (mod a) \<longleftrightarrow> b mod a = c mod a"
-abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(1[_ \<noteq> _] '(' mod _'))\<close>)
- where "notcong b c a \<equiv> \<not> cong b c a"
+abbreviation notcong :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+ (\<open>(\<open>indent=1 notation=\<open>mixfix notcong\<close>\<close>[_ \<noteq> _] '(' mod _'))\<close>)
+ where "[b \<noteq> c] (mod a) \<equiv> \<not> cong b c a"
lemma cong_refl [simp]:
"[b = b] (mod a)"