NEWS: [arith]
authornipkow
Tue Mar 24 14:08:13 2009 +0100 (2009-03-24)
changeset 30706e20227b5e6a3
parent 30699 08760e217eb7
child 30707 b0391b9b7103
NEWS: [arith]
NEWS
     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.