--- a/src/HOL/Fun.thy Sun Oct 06 22:56:07 2024 +0200
+++ b/src/HOL/Fun.thy Tue Oct 08 12:10:35 2024 +0200
@@ -844,7 +844,8 @@
"_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind" (\<open>(\<open>indent=2 notation=\<open>mixfix update\<close>\<close>_ :=/ _)\<close>)
"" :: "updbind \<Rightarrow> updbinds" (\<open>_\<close>)
"_updbinds":: "updbind \<Rightarrow> updbinds \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
- "_Update" :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a" (\<open>_/'((2_)')\<close> [1000, 0] 900)
+ "_Update" :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a"
+ (\<open>(\<open>open_block notation=\<open>mixfix function update\<close>\<close>_/'((2_)'))\<close> [1000, 0] 900)
translations
"_Update f (_updbinds b bs)" \<rightleftharpoons> "_Update (_Update f b) bs"