--- a/src/HOL/Fun.thy Sun Aug 25 12:43:43 2024 +0200
+++ b/src/HOL/Fun.thy Sun Aug 25 15:02:19 2024 +0200
@@ -846,6 +846,9 @@
"_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" ("_,/ _")
"_Update" :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a" ("_/'((_)')" [1000, 0] 900)
+syntax_consts
+ "_updbind" "_updbinds" "_Update" \<rightleftharpoons> fun_upd
+
translations
"_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs"
"f(x:=y)" \<rightleftharpoons> "CONST fun_upd f x y"