author | nipkow |
Tue, 23 Jun 1998 18:09:16 +0200 | |
changeset 5072 | 255324b49a1c |
parent 5071 | 548f398d770b |
child 5073 | 61e4403023a2 |
--- 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