diff -r 4641f0fdaa59 -r be8c0e039a5e src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Filter.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -41,6 +41,8 @@
 
 syntax
   "_eventually" :: "pttrn => 'a filter => bool => bool"  ("(3\<forall>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
+syntax_consts
+  "_eventually" == eventually
 translations
   "\<forall>\<^sub>Fx in F. P" == "CONST eventually (\<lambda>x. P) F"
 
@@ -159,6 +161,8 @@
 
 syntax
   "_frequently" :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<exists>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
+syntax_consts
+  "_frequently" == frequently
 translations
   "\<exists>\<^sub>Fx in F. P" == "CONST frequently (\<lambda>x. P) F"
 
@@ -1305,6 +1309,9 @@
 syntax
   "_LIM" :: "pttrns \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> bool" ("(3LIM (_)/ (_)./ (_) :> (_))" [1000, 10, 0, 10] 10)
 
+syntax_consts
+  "_LIM" == filterlim
+
 translations
   "LIM x F1. f :> F2" == "CONST filterlim (\<lambda>x. f) F2 F1"