--- a/src/ZF/func.thy Fri Aug 23 22:47:51 2024 +0200
+++ b/src/ZF/func.thy Fri Aug 23 23:14:39 2024 +0200
@@ -448,18 +448,14 @@
nonterminal updbinds and updbind
syntax
-
- (* Let expressions *)
-
"_updbind" :: "[i, i] \<Rightarrow> updbind" (\<open>(2_ :=/ _)\<close>)
"" :: "updbind \<Rightarrow> updbinds" (\<open>_\<close>)
"_updbinds" :: "[updbind, updbinds] \<Rightarrow> updbinds" (\<open>_,/ _\<close>)
"_Update" :: "[i, updbinds] \<Rightarrow> i" (\<open>_/'((_)')\<close> [900,0] 900)
-
translations
"_Update (f, _updbinds(b,bs))" == "_Update (_Update(f,b), bs)"
"f(x:=y)" == "CONST update(f,x,y)"
-
+syntax_consts "_Update" "_updbind" \<rightleftharpoons> update
lemma update_apply [simp]: "f(x:=y) ` z = (if z=x then y else f`z)"
apply (simp add: update_def)