NEWS
changeset 5072 255324b49a1c
parent 5059 dcdb21e53537
child 5075 9a3d48fa28ca
--- a/NEWS	Tue Jun 23 18:07:45 1998 +0200
+++ b/NEWS	Tue Jun 23 18:09:16 1998 +0200
@@ -65,7 +65,8 @@
 * 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
+  f(a:=b) == %x. if x=a then b else f x
+  May also be iterated as in f(a:=b,c:=d,...).
 
 * New directory HOL/UNITY: Chandy and Misra's UNITY formalism