--- a/src/ZF/func.thy Sun Sep 29 21:40:37 2024 +0200
+++ b/src/ZF/func.thy Sun Sep 29 21:57:47 2024 +0200
@@ -452,7 +452,8 @@
"" :: "updbind \<Rightarrow> updbinds" (\<open>_\<close>)
"_updbinds" :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
"_Update" :: "[i, updbinds] \<Rightarrow> i" (\<open>_/'((_)')\<close> [900,0] 900)
-syntax_consts "_Update" "_updbind" \<rightleftharpoons> update
+syntax_consts
+ update
translations
"_Update (f, _updbinds(b,bs))" == "_Update (_Update(f,b), bs)"
"f(x:=y)" == "CONST update(f,x,y)"