Map.update -> map_upd, Unpdate.update -> fun_upd
Problem: macros get confused about two updates.
(* Title: HOL/Update.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
Function updates: like theory Map, but for ordinary functions
*)
Update = Fun +
consts
fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
nonterminals
updbinds updbind
syntax
(* Let expressions *)
"_updbind" :: ['a, 'a] => updbind ("(2_ :=/ _)")
"" :: updbind => updbinds ("_")
"_updbinds" :: [updbind, updbinds] => updbinds ("_,/ _")
"_Update" :: ['a, updbinds] => 'a ("_/'((_)')" [900,0] 900)
translations
"_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"
"f(x:=y)" == "fun_upd f x y"
defs
fun_upd_def "f(a:=b) == %x. if x=a then b else f x"
end