# HG changeset patch
# User wenzelm
# Date 1237907502 -3600
# Node ID 83df88b6d082f3537a23f305d914b70d4faf546a
# Parent  b0391b9b710376b236067ae6366ef79c13318da6# Parent  e8ab35c6ade6ff88d0aaaffc6c74975a0efb92f8
merged

diff -r e8ab35c6ade6 -r 83df88b6d082 NEWS
--- a/NEWS	Tue Mar 24 16:11:09 2009 +0100
+++ b/NEWS	Tue Mar 24 16:11:42 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.