--- a/src/HOL/Fun.thy Mon Sep 23 15:01:10 2024 +0200
+++ b/src/HOL/Fun.thy Mon Sep 23 21:09:23 2024 +0200
@@ -841,10 +841,10 @@
nonterminal updbinds and updbind
syntax
- "_updbind" :: "'a \<Rightarrow> 'a \<Rightarrow> updbind" (\<open>(2_ :=/ _)\<close>)
+ "_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>_/'((_)')\<close> [1000, 0] 900)
+ "_Update" :: "'a \<Rightarrow> updbinds \<Rightarrow> 'a" (\<open>_/'((\<open>indent=2 notation=\<open>mixfix updates\<close>\<close>_)')\<close> [1000, 0] 900)
syntax_consts
"_updbind" "_updbinds" "_Update" \<rightleftharpoons> fun_upd