--- 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