*** empty log message ***
authornipkow
Tue, 23 Jun 1998 18:09:16 +0200
changeset 5072 255324b49a1c
parent 5071 548f398d770b
child 5073 61e4403023a2
*** empty log message ***
NEWS
--- 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