changeset 4899 | 447d6b2956ba |
parent 4880 | 312115d20c45 |
child 4915 | 5ff99bd60da9 |
--- a/NEWS Wed May 06 13:01:30 1998 +0200 +++ b/NEWS Wed May 06 13:01:45 1998 +0200 @@ -48,6 +48,9 @@ * 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 + * New directory HOL/UNITY: Chandy and Misra's UNITY formalism * split_all_tac is now much faster and fails if there is nothing to