changeset 5072 | 255324b49a1c |
parent 5059 | dcdb21e53537 |
child 5075 | 9a3d48fa28ca |
--- a/NEWS Tue Jun 23 18:07:45 1998 +0200 +++ b/NEWS Tue Jun 23 18:09:16 1998 +0200 @@ -65,7 +65,8 @@ * 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 + f(a:=b) == %x. if x=a then b else f x + May also be iterated as in f(a:=b,c:=d,...). * New directory HOL/UNITY: Chandy and Misra's UNITY formalism