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) -------------------------------