# HG changeset patch
# User wenzelm
# Date 1727642834 -7200
# Node ID 216e55ebac94e9585d249eee596618786ae0f933
# Parent  6d34c2bedaa3835be1a5985c408a8d2ec19472ff
tuned markup;

diff -r 6d34c2bedaa3 -r 216e55ebac94 src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Sun Sep 29 21:57:47 2024 +0200
+++ b/src/ZF/Induct/Multiset.thy	Sun Sep 29 22:47:14 2024 +0200
@@ -74,7 +74,7 @@
   "a :# M \<equiv> a \<in> mset_of(M)"
 
 syntax
-  "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix MCollect\<close>\<close>{# _ \<in> _./ _#})\<close>)
+  "_MColl" :: "[pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix multiset comprehension\<close>\<close>{# _ \<in> _./ _#})\<close>)
 syntax_consts
   MCollect
 translations
diff -r 6d34c2bedaa3 -r 216e55ebac94 src/ZF/ZF_Base.thy
--- a/src/ZF/ZF_Base.thy	Sun Sep 29 21:57:47 2024 +0200
+++ b/src/ZF/ZF_Base.thy	Sun Sep 29 22:47:14 2024 +0200
@@ -55,7 +55,7 @@
   where "Replace(A,P) \<equiv> PrimReplace(A, \<lambda>x y. (\<exists>!z. P(x,z)) \<and> P(x,y))"
 
 syntax
-  "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix Replace\<close>\<close>{_ ./ _ \<in> _, _})\<close>)
+  "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix relational replacement\<close>\<close>{_ ./ _ \<in> _, _})\<close>)
 syntax_consts
   Replace
 translations
@@ -68,7 +68,7 @@
   where "RepFun(A,f) \<equiv> {y . x\<in>A, y=f(x)}"
 
 syntax
-  "_RepFun" :: "[i, pttrn, i] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix RepFun\<close>\<close>{_ ./ _ \<in> _})\<close> [51,0,51])
+  "_RepFun" :: "[i, pttrn, i] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix functional replacement\<close>\<close>{_ ./ _ \<in> _})\<close> [51,0,51])
 syntax_consts
   RepFun
 translations
@@ -80,7 +80,7 @@
   where "Collect(A,P) \<equiv> {y . x\<in>A, x=y \<and> P(x)}"
 
 syntax
-  "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_ \<in> _ ./ _})\<close>)
+  "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{_ \<in> _ ./ _})\<close>)
 syntax_consts
   Collect
 translations
@@ -299,9 +299,9 @@
 syntax (ASCII)
   "_Ball"     :: "[pttrn, i, o] \<Rightarrow> o"        (\<open>(\<open>indent=3 notation=\<open>binder ALL:\<close>\<close>ALL _:_./ _)\<close> 10)
   "_Bex"      :: "[pttrn, i, o] \<Rightarrow> o"        (\<open>(\<open>indent=3 notation=\<open>binder EX:\<close>\<close>EX _:_./ _)\<close> 10)
-  "_Collect"  :: "[pttrn, i, o] \<Rightarrow> i"        (\<open>(\<open>indent=1 notation=\<open>mixfix Collect\<close>\<close>{_: _ ./ _})\<close>)
-  "_Replace"  :: "[pttrn, pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix Replace\<close>\<close>{_ ./ _: _, _})\<close>)
-  "_RepFun"   :: "[i, pttrn, i] \<Rightarrow> i"        (\<open>(\<open>indent=1 notation=\<open>mixfix RepFun\<close>\<close>{_ ./ _: _})\<close> [51,0,51])
+  "_Collect"  :: "[pttrn, i, o] \<Rightarrow> i"        (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{_: _ ./ _})\<close>)
+  "_Replace"  :: "[pttrn, pttrn, i, o] \<Rightarrow> i" (\<open>(\<open>indent=1 notation=\<open>mixfix relational replacement\<close>\<close>{_ ./ _: _, _})\<close>)
+  "_RepFun"   :: "[i, pttrn, i] \<Rightarrow> i"        (\<open>(\<open>indent=1 notation=\<open>mixfix functional replacement\<close>\<close>{_ ./ _: _})\<close> [51,0,51])
   "_UNION"    :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(\<open>indent=3 notation=\<open>binder UN:\<close>\<close>UN _:_./ _)\<close> 10)
   "_INTER"    :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(\<open>indent=3 notation=\<open>binder INT:\<close>\<close>INT _:_./ _)\<close> 10)
   "_PROD"     :: "[pttrn, i, i] \<Rightarrow> i"        (\<open>(\<open>indent=3 notation=\<open>binder PROD:\<close>\<close>PROD _:_./ _)\<close> 10)