src/HOL/Set.thy

--- a/src/HOL/Set.thy	Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Set.thy	Sun Aug 25 15:02:19 2024 +0200
@@ -40,6 +40,8 @@
 
 syntax
   "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set"    ("(1{_./ _})")
+syntax_consts
+  "_Coll" \<rightleftharpoons> Collect
 translations
   "{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
 
@@ -47,6 +49,8 @@
   "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{(_/: _)./ _})")
 syntax
   "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{(_/ \<in> _)./ _})")
+syntax_consts
+  "_Collect" \<rightleftharpoons> Collect
 translations
   "{p:A. P}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"
 
@@ -141,6 +145,8 @@
 
 syntax
   "_Finset" :: "args \<Rightarrow> 'a set"    ("{(_)}")
+syntax_consts
+  "_Finset" \<rightleftharpoons> insert
 translations
   "{x, xs}" \<rightleftharpoons> "CONST insert x {xs}"
   "{x}" \<rightleftharpoons> "CONST insert x {}"
@@ -203,6 +209,12 @@
   "_Bex1"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>!(_/\<in>_)./ _)" [0, 0, 10] 10)
   "_Bleast"     :: "id \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a"           ("(3LEAST(_/\<in>_)./ _)" [0, 0, 10] 10)
 
+syntax_consts
+  "_Ball" \<rightleftharpoons> Ball and
+  "_Bex" \<rightleftharpoons> Bex and
+  "_Bex1" \<rightleftharpoons> Ex1 and
+  "_Bleast" \<rightleftharpoons> Least
+
 translations
   "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball A (\<lambda>x. P)"
   "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex A (\<lambda>x. P)"
@@ -223,6 +235,11 @@
   "_setleEx"    :: "[idt, 'a, bool] \<Rightarrow> bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
   "_setleEx1"   :: "[idt, 'a, bool] \<Rightarrow> bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
 
+syntax_consts
+  "_setlessAll" "_setleAll" \<rightleftharpoons> All and
+  "_setlessEx" "_setleEx" \<rightleftharpoons> Ex and
+  "_setleEx1" \<rightleftharpoons> Ex1
+
 translations
  "\<forall>A\<subset>B. P" \<rightharpoonup> "\<forall>A. A \<subset> B \<longrightarrow> P"
  "\<exists>A\<subset>B. P" \<rightharpoonup> "\<exists>A. A \<subset> B \<and> P"
@@ -272,6 +289,8 @@
 
 syntax
   "_Setcompr" :: "'a \<Rightarrow> idts \<Rightarrow> bool \<Rightarrow> 'a set"    ("(1{_ |/_./ _})")
+syntax_consts
+  "_Setcompr" \<rightleftharpoons> Collect
 
 parse_translation \<open>
   let