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