--- a/src/ZF/func.thy Sun Oct 06 22:56:07 2024 +0200
+++ b/src/ZF/func.thy Tue Oct 08 12:10:35 2024 +0200
@@ -448,10 +448,10 @@
nonterminal updbinds and updbind
syntax
- "_updbind" :: "[i, i] \<Rightarrow> updbind" (\<open>(\<open>indent=2 notation=\<open>infix update\<close>\<close>_ :=/ _)\<close>)
- "" :: "updbind \<Rightarrow> updbinds" (\<open>_\<close>)
- "_updbinds" :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
- "_Update" :: "[i, updbinds] \<Rightarrow> i" (\<open>_/'((_)')\<close> [900,0] 900)
+ "_updbind" :: "[i, i] \<Rightarrow> updbind" (\<open>(\<open>indent=2 notation=\<open>infix update\<close>\<close>_ :=/ _)\<close>)
+ "" :: "updbind \<Rightarrow> updbinds" (\<open>_\<close>)
+ "_updbinds" :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
+ "_Update" :: "[i, updbinds] \<Rightarrow> i" (\<open>(\<open>open_block notation=\<open>mixfix function update\<close>\<close>_/'((_)'))\<close> [900,0] 900)
translations
"_Update (f, _updbinds(b,bs))" == "_Update (_Update(f,b), bs)"
"f(x:=y)" == "CONST update(f,x,y)"