--- a/src/HOL/Analysis/Sparse_In.thy Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Sparse_In.thy Sun Aug 25 21:10:01 2024 +0200
@@ -166,11 +166,15 @@
syntax
"_eventually_cosparse" :: "pttrn => 'a set => bool => bool" ("(3\<forall>\<^sub>\<approx>_\<in>_./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_eventually_cosparse" == eventually
translations
"\<forall>\<^sub>\<approx>x\<in>A. P" == "CONST eventually (\<lambda>x. P) (CONST cosparse A)"
syntax
"_qeventually_cosparse" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3\<forall>\<^sub>\<approx>_ | (_)./ _)" [0, 0, 10] 10)
+syntax_consts
+ "_qeventually_cosparse" == eventually
translations
"\<forall>\<^sub>\<approx>x|P. t" => "CONST eventually (\<lambda>x. t) (CONST cosparse {x. P})"