# HG changeset patch
# User wenzelm
# Date 1727876208 -7200
# Node ID 8e66b4be036f7efb8af636aca9d587f377a6c0fa
# Parent  739b99d0911a710f5560c10723a68795332fb6a1
more inner syntax markup;

diff -r 739b99d0911a -r 8e66b4be036f src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Wed Oct 02 14:23:28 2024 +0200
+++ b/src/HOL/Library/FSet.thy	Wed Oct 02 15:36:48 2024 +0200
@@ -192,15 +192,15 @@
 end
 
 syntax (input)
-  "_fBall"       :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3! (_/|:|_)./ _)\<close> [0, 0, 10] 10)
-  "_fBex"        :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3? (_/|:|_)./ _)\<close> [0, 0, 10] 10)
-  "_fBex1"       :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3?! (_/:_)./ _)\<close> [0, 0, 10] 10)
+  "_fBall" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder finite !\<close>\<close>! (_/|:|_)./ _)\<close> [0, 0, 10] 10)
+  "_fBex"  :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder finite ?\<close>\<close>? (_/|:|_)./ _)\<close> [0, 0, 10] 10)
+  "_fBex1" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder finite ?!\<close>\<close>?! (_/:_)./ _)\<close> [0, 0, 10] 10)
 
 syntax
-  "_fBall"       :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3\<forall>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
-  "_fBex"        :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3\<exists>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
-  "_fBnex"       :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3\<nexists>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
-  "_fBex1"       :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"      (\<open>(3\<exists>!(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
+  "_fBall" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder finite \<forall>\<close>\<close>\<forall>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
+  "_fBex"  :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder finite \<exists>\<close>\<close>\<exists>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
+  "_fBnex" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder finite \<nexists>\<close>\<close>\<nexists>(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
+  "_fBex1" :: "pttrn \<Rightarrow> 'a fset \<Rightarrow> bool \<Rightarrow> bool"  (\<open>(\<open>indent=3 notation=\<open>binder finite \<exists>!\<close>\<close>\<exists>!(_/|\<in>|_)./ _)\<close> [0, 0, 10] 10)
 
 syntax_consts
   "_fBall" "_fBnex" \<rightleftharpoons> fBall and
@@ -219,10 +219,10 @@
 \<close> \<comment> \<open>to avoid eta-contraction of body\<close>
 
 syntax
-  "_setlessfAll" :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(3\<forall>_|\<subset>|_./ _)\<close>  [0, 0, 10] 10)
-  "_setlessfEx"  :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(3\<exists>_|\<subset>|_./ _)\<close>  [0, 0, 10] 10)
-  "_setlefAll"   :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(3\<forall>_|\<subseteq>|_./ _)\<close> [0, 0, 10] 10)
-  "_setlefEx"    :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(3\<exists>_|\<subseteq>|_./ _)\<close> [0, 0, 10] 10)
+  "_setlessfAll" :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(\<open>indent=3 notation=\<open>binder finite \<forall>\<close>\<close>\<forall>_|\<subset>|_./ _)\<close>  [0, 0, 10] 10)
+  "_setlessfEx"  :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(\<open>indent=3 notation=\<open>binder finite \<exists>\<close>\<close>\<exists>_|\<subset>|_./ _)\<close>  [0, 0, 10] 10)
+  "_setlefAll"   :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(\<open>indent=3 notation=\<open>binder finite \<forall>\<close>\<close>\<forall>_|\<subseteq>|_./ _)\<close> [0, 0, 10] 10)
+  "_setlefEx"    :: "[idt, 'a, bool] \<Rightarrow> bool"   (\<open>(\<open>indent=3 notation=\<open>binder finite \<exists>\<close>\<close>\<exists>_|\<subseteq>|_./ _)\<close> [0, 0, 10] 10)
 
 syntax_consts
   "_setlessfAll" "_setlefAll" \<rightleftharpoons> All and