HOL/Update
authorpaulson
Wed May 06 13:01:45 1998 +0200 (1998-05-06)
changeset 4899447d6b2956ba
parent 4898 68fd1a2b8b7b
child 4900 a4301a63bf5c
HOL/Update
NEWS
     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