NEWS
changeset 30706 e20227b5e6a3
parent 30609 983e8b6e4e69
child 30728 f0aeca99b5d9
child 30740 2d3ae5a7edb2
     1.1 --- a/NEWS	Tue Mar 24 13:13:18 2009 +0100
     1.2 +++ b/NEWS	Tue Mar 24 14:08:13 2009 +0100
     1.3 @@ -330,6 +330,11 @@
     1.4  * Simplifier: simproc for let expressions now unfolds if bound variable
     1.5  occurs at most once in let expression body.  INCOMPATIBILITY.
     1.6  
     1.7 +* New attribute "arith" for facts that should always be used automaticaly
     1.8 +by arithmetic. It is intended to be used locally in proofs, eg
     1.9 +assumes [arith]: "x > 0"
    1.10 +Global usage is discouraged because of possible performance impact.
    1.11 +
    1.12  * New classes "top" and "bot" with corresponding operations "top" and "bot"
    1.13  in theory Orderings;  instantiation of class "complete_lattice" requires
    1.14  instantiation of classes "top" and "bot".  INCOMPATIBILITY.