src/ZF/ZF_Base.thy

--- a/src/ZF/ZF_Base.thy	Fri Oct 18 11:44:05 2024 +0200
+++ b/src/ZF/ZF_Base.thy	Fri Oct 18 14:20:09 2024 +0200
@@ -56,6 +56,8 @@
 
 syntax
   "_Replace" :: "[pttrn, pttrn, i, o] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix relational replacement\<close>\<close>{_ ./ _ \<in> _, _})\<close>)
+syntax_consts
+  "_Replace" \<rightleftharpoons> Replace
 translations
   "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
 
@@ -67,6 +69,8 @@
 
 syntax
   "_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" \<rightleftharpoons> RepFun
 translations
   "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
 
@@ -77,6 +81,8 @@
 
 syntax
   "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  (\<open>(\<open>indent=1 notation=\<open>mixfix set comprehension\<close>\<close>{_ \<in> _ ./ _})\<close>)
+syntax_consts
+  "_Collect" \<rightleftharpoons> Collect
 translations
   "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"