NEWS
changeset 5072 255324b49a1c
parent 5059 dcdb21e53537
child 5075 9a3d48fa28ca
     1.1 --- a/NEWS	Tue Jun 23 18:07:45 1998 +0200
     1.2 +++ b/NEWS	Tue Jun 23 18:09:16 1998 +0200
     1.3 @@ -65,7 +65,8 @@
     1.4  * added option_map_eq_Some to simpset() and claset()
     1.5  
     1.6  * New theory HOL/Update of function updates:
     1.7 -  f[a:=b] == %x. if x=a then b else f x
     1.8 +  f(a:=b) == %x. if x=a then b else f x
     1.9 +  May also be iterated as in f(a:=b,c:=d,...).
    1.10  
    1.11  * New directory HOL/UNITY: Chandy and Misra's UNITY formalism
    1.12