diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Number_Theory/Cong.thy
--- 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)"