# HG changeset patch
# User desharna
# Date 1711615311 -3600
# Node ID 67e77f1e6d7bd7b4c5546673c46e9a03c935cdd9
# Parent  804a41d08b8420baa9ee90a8e5b5b189120143a6
added special syntax for FSet.Ball and FSet.Bex

diff -r 804a41d08b84 -r 67e77f1e6d7b src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Thu Mar 28 09:40:58 2024 +0100
+++ b/src/HOL/Library/FSet.thy	Thu Mar 28 09:41:51 2024 +0100
@@ -192,6 +192,23 @@
 
 end
 
+syntax (input)
+  "_fBall"       :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      ("(3! (_/|:|_)./ _)" [0, 0, 10] 10)
+  "_fBex"        :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      ("(3? (_/|:|_)./ _)" [0, 0, 10] 10)
+
+syntax
+  "_fBall"       :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>(_/|\<in>|_)./ _)" [0, 0, 10] 10)
+  "_fBex"        :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>(_/|\<in>|_)./ _)" [0, 0, 10] 10)
+
+translations
+  "\<forall>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Ball A (\<lambda>x. P)"
+  "\<exists>x|\<in>|A. P" \<rightleftharpoons> "CONST FSet.Bex A (\<lambda>x. P)"
+
+print_translation \<open>
+ [Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>fBall\<close> \<^syntax_const>\<open>_fBall\<close>,
+  Syntax_Trans.preserve_binder_abs2_tr' \<^const_syntax>\<open>fBex\<close> \<^syntax_const>\<open>_fBex\<close>]
+\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
+
 context includes lifting_syntax
 begin