--- a/src/HOL/Update.ML Wed May 06 11:46:00 1998 +0200
+++ b/src/HOL/Update.ML Wed May 06 13:01:30 1998 +0200
@@ -1,9 +1,9 @@
-(* Title: HOL/UNITY/Update.thy
+(* Title: HOL/Update.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Function updates: like the standard theory Map, but for ordinary functions
+Function updates: like theory Map, but for ordinary functions
*)
open Update;
--- a/src/HOL/Update.thy Wed May 06 11:46:00 1998 +0200
+++ b/src/HOL/Update.thy Wed May 06 13:01:30 1998 +0200
@@ -1,9 +1,9 @@
-(* Title: HOL/UNITY/Update.thy
+(* Title: HOL/Update.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
-Function updates: like the standard theory Map, but for ordinary functions
+Function updates: like theory Map, but for ordinary functions
*)
Update = Fun +
@@ -12,10 +12,6 @@
update :: "('a => 'b) => 'a => 'b => ('a => 'b)"
("_/[_/:=/_]" [900,0,0] 900)
-syntax (symbols)
- update :: "('a => 'b) => 'a => 'b => ('a => 'b)"
- ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
-
defs
update_def "f[a:=b] == %x. if x=a then b else f x"