diff -r ff2a637a449e -r fc5066122e68 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/HOL/Filter.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -1308,10 +1308,8 @@
 
 syntax
   "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" (\<open>(\<open>indent=3 notation=\<open>binder LIM\<close>\<close>LIM (_)/ (_)./ (_) :> (_))\<close> [1000, 10, 0, 10] 10)
-
 syntax_consts
   "_LIM" == filterlim
-
 translations
   "LIM x F1. f :> F2" == "CONST filterlim (\<lambda>x. f) F2 F1"