--- a/NEWS Wed Mar 12 22:57:50 2014 +0100
+++ b/NEWS Thu Mar 13 07:07:07 2014 +0100
@@ -98,6 +98,12 @@
*** HOL ***
+* Simplifier: Enhanced solver of preconditions of rewrite rules
+ can now deal with conjunctions.
+ For help with converting proofs, the old behaviour of the simplifier
+ can be restored like this: declare/using [[simp_legacy_precond]]
+ This configuration option will disappear again in the future.
+
* HOL-Word:
* Abandoned fact collection "word_arith_alts", which is a
duplicate of "word_arith_wis".