--- a/src/HOL/Update.thy Fri Jul 24 14:53:23 1998 +0200
+++ b/src/HOL/Update.thy Fri Jul 24 17:18:15 1998 +0200
@@ -9,7 +9,7 @@
Update = Fun +
consts
- update :: "('a => 'b) => 'a => 'b => ('a => 'b)"
+ fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)"
nonterminals
updbinds updbind
@@ -25,9 +25,9 @@
translations
"_Update f (_updbinds b bs)" == "_Update (_Update f b) bs"
- "f(x:=y)" == "update f x y"
+ "f(x:=y)" == "fun_upd f x y"
defs
- update_def "f(a:=b) == %x. if x=a then b else f x"
+ fun_upd_def "f(a:=b) == %x. if x=a then b else f x"
end