src/HOL/Update.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Update.thy	Tue May 05 17:28:22 1998 +0200
@@ -0,0 +1,22 @@
+(*  Title:      HOL/UNITY/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
+*)
+
+Update = Fun +
+
+consts
+  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"
+
+end