NEWS
changeset 4899 447d6b2956ba
parent 4880 312115d20c45
child 4915 5ff99bd60da9
     1.1 --- a/NEWS	Wed May 06 13:01:30 1998 +0200
     1.2 +++ b/NEWS	Wed May 06 13:01:45 1998 +0200
     1.3 @@ -48,6 +48,9 @@
     1.4  
     1.5  * added option_map_eq_Some to simpset() and claset()
     1.6  
     1.7 +* New theory HOL/Update of function updates:
     1.8 +  f[a:=b] == %x. if x=a then b else f x
     1.9 +
    1.10  * New directory HOL/UNITY: Chandy and Misra's UNITY formalism
    1.11  
    1.12  * split_all_tac is now much faster and fails if there is nothing to