--- a/src/HOL/Set.thy Tue Oct 01 23:36:10 2024 +0200
+++ b/src/HOL/Set.thy Wed Oct 02 10:34:41 2024 +0200
@@ -39,18 +39,14 @@
text \<open>Set comprehensions\<close>
syntax
- "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_./ _})\<close>)
-syntax_consts
- "_Coll" \<rightleftharpoons> Collect
+ "_Coll" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{_./ _})\<close>)
translations
"{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
syntax (ASCII)
- "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{(_/: _)./ _})\<close>)
+ "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{(_/: _)./ _})\<close>)
syntax
- "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{(_/ \<in> _)./ _})\<close>)
-syntax_consts
- "_Collect" \<rightleftharpoons> Collect
+ "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set" (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{(_/ \<in> _)./ _})\<close>)
translations
"{p:A. P}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"