HOL/Update

--- a/NEWS	Wed May 06 13:01:30 1998 +0200
+++ b/NEWS	Wed May 06 13:01:45 1998 +0200
@@ -48,6 +48,9 @@
 
 * added option_map_eq_Some to simpset() and claset()
 
+* New theory HOL/Update of function updates:
+  f[a:=b] == %x. if x=a then b else f x
+
 * New directory HOL/UNITY: Chandy and Misra's UNITY formalism
 
 * split_all_tac is now much faster and fails if there is nothing to