# HG changeset patch
# User nipkow
# Date 1237900093 -3600
# Node ID e20227b5e6a37d56ac499c93caa5781ab4ca0c46
# Parent  08760e217eb7729050f6e2213115c96bf122efc6
NEWS: [arith]

diff -r 08760e217eb7 -r e20227b5e6a3 NEWS
--- 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.