# HG changeset patch
# User nipkow
# Date 1237900164 -3600
# Node ID b0391b9b710376b236067ae6366ef79c13318da6
# Parent  9ae91c0d3d1b966a246acac65fda0d4ea81087d8# Parent  e20227b5e6a37d56ac499c93caa5781ab4ca0c46
merged

diff -r 9ae91c0d3d1b -r b0391b9b7103 NEWS
--- a/NEWS	Tue Mar 24 13:20:40 2009 +0100
+++ b/NEWS	Tue Mar 24 14:09:24 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.