NEWS
changeset 5490 85855f65d0c6
parent 5475 410172655d64
child 5524 38f2a518a811
     1.1 --- a/NEWS	Tue Sep 15 13:09:23 1998 +0200
     1.2 +++ b/NEWS	Tue Sep 15 15:04:07 1998 +0200
     1.3 @@ -20,6 +20,8 @@
     1.4    less_imp_add_less  should be replaced by  trans_less_add1
     1.5    le_imp_add_le      should be replaced by  trans_le_add1
     1.6  
     1.7 +* HOL: unary - is now overloaded (new type constraints may be required);
     1.8 +
     1.9  * Pure: ML function 'theory_of' replaced by 'theory';
    1.10  
    1.11  
    1.12 @@ -209,6 +211,10 @@
    1.13  * HOL/recdef can now declare non-recursive functions, with {} supplied as
    1.14  the well-founded relation;
    1.15  
    1.16 +* HOL/Set INCOMPATIBILITY: the complement of set A is now written -A instead of
    1.17 +    Compl A.  The "Compl" syntax remains available as input syntax for this
    1.18 +    release ONLY.
    1.19 +
    1.20  * HOL/Update: new theory of function updates:
    1.21      f(a:=b) == %x. if x=a then b else f x
    1.22  may also be iterated as in f(a:=b,c:=d,...);