--- a/src/HOL/Library/Real_Mod.thy	Sat Mar 30 01:12:48 2024 +0100
+++ b/src/HOL/Library/Real_Mod.thy	Fri Mar 29 19:28:59 2024 +0100
@@ -7,6 +7,8 @@
   imports Complex_Main
 begin
 
+(* MOVED TO HOL-Library ON 20.03.2024 *)
+
 definition rmod :: "real \<Rightarrow> real \<Rightarrow> real" (infixl "rmod" 70) where
   "x rmod y = x - \<bar>y\<bar> * of_int \<lfloor>x / \<bar>y\<bar>\<rfloor>"