NEWS
changeset 5077 71043526295f
parent 5075 9a3d48fa28ca
child 5085 8e5a7942fdea
     1.1 --- a/NEWS	Wed Jun 24 11:24:52 1998 +0200
     1.2 +++ b/NEWS	Wed Jun 24 13:59:45 1998 +0200
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  Isabelle NEWS -- history of user-visible changes
     1.6  ================================================
     1.7  
     1.8 @@ -56,11 +55,14 @@
     1.9  
    1.10  * added option_map_eq_Some to simpset() and claset()
    1.11  
    1.12 +* New directory HOL/UNITY: Chandy and Misra's UNITY formalism
    1.13 +
    1.14  * New theory HOL/Update of function updates:
    1.15    f(a:=b) == %x. if x=a then b else f x
    1.16    May also be iterated as in f(a:=b,c:=d,...).
    1.17  
    1.18 -* New directory HOL/UNITY: Chandy and Misra's UNITY formalism
    1.19 +* HOL/List: new function list_update written xs[i:=v] that updates the i-th
    1.20 +  list position. May also be iterated as in xs[i:=a,j:=b,...].
    1.21  
    1.22  * split_all_tac is now much faster and fails if there is nothing to
    1.23  split.  Existing (fragile) proofs may require adaption because the