--- a/NEWS Tue Mar 24 13:13:18 2009 +0100
+++ b/NEWS Tue Mar 24 14:08:13 2009 +0100
@@ -330,6 +330,11 @@
* Simplifier: simproc for let expressions now unfolds if bound variable
occurs at most once in let expression body. INCOMPATIBILITY.
+* New attribute "arith" for facts that should always be used automaticaly
+by arithmetic. It is intended to be used locally in proofs, eg
+assumes [arith]: "x > 0"
+Global usage is discouraged because of possible performance impact.
+
* New classes "top" and "bot" with corresponding operations "top" and "bot"
in theory Orderings; instantiation of class "complete_lattice" requires
instantiation of classes "top" and "bot". INCOMPATIBILITY.