NEWS
changeset 70347 e5cd5471c18a
parent 70342 e4d626692640
child 70434 4abd07cd034f
--- a/NEWS	Fri Jun 14 08:34:28 2019 +0000
+++ b/NEWS	Fri Jun 14 08:34:28 2019 +0000
@@ -18,6 +18,11 @@
 Z2 (0 / 1): theory HOL/Library/Bit.thy has been renamed accordingly.
 INCOMPATIBILITY.
 
+* Fact collection sign_simps contains only simplification rules
+for products being less / greater / equal to zero; combine with
+existing collections algebra_simps or field_simps to obtain
+reasonable simplification.  INCOMPATIBILITY.
+
 
 New in Isabelle2019 (June 2019)
 -------------------------------