--- a/src/HOL/Fun.thy Sat Dec 14 23:48:45 2024 +0100
+++ b/src/HOL/Fun.thy Sun Dec 15 14:59:57 2024 +0100
@@ -840,6 +840,9 @@
nonterminal updbinds and updbind
+open_bundle update_syntax
+begin
+
syntax
"_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind" (\<open>(\<open>indent=2 notation=\<open>mixfix update\<close>\<close>_ :=/ _)\<close>)
"" :: "updbind \<Rightarrow> updbinds" (\<open>_\<close>)
@@ -852,6 +855,8 @@
"_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs"
"f(x:=y)" \<rightleftharpoons> "CONST fun_upd f x y"
+end
+
(* Hint: to define the sum of two functions (or maps), use case_sum.
A nice infix syntax could be defined by
notation