diff -r 3e3e7a68cd80 -r 6ad2c917dd2e src/HOL/Library/Real_Mod.thy
--- a/src/HOL/Library/Real_Mod.thy	Wed Oct 09 22:01:33 2024 +0200
+++ b/src/HOL/Library/Real_Mod.thy	Wed Oct 09 23:38:29 2024 +0200
@@ -106,8 +106,9 @@
 
 
 
-definition rcong :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool" (\<open>(1[_ = _] '(' rmod _'))\<close>) where
-  "[x = y] (rmod m) \<longleftrightarrow> x rmod m = y rmod m"
+definition rcong :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool"
+    (\<open>(\<open>indent=1 notation=\<open>mixfix rcong\<close>\<close>[_ = _] '(' rmod _'))\<close>)
+  where "[x = y] (rmod m) \<longleftrightarrow> x rmod m = y rmod m"
 
 named_theorems rcong_intros