NEWS
changeset 56073 29e308b56d23
parent 56072 31e427387ab5
child 56076 e52fc7c37ed3
     1.1 --- a/NEWS	Wed Mar 12 22:57:50 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 13 07:07:07 2014 +0100
     1.3 @@ -98,6 +98,12 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Simplifier: Enhanced solver of preconditions of rewrite rules
     1.8 +  can now deal with conjunctions.
     1.9 +  For help with converting proofs, the old behaviour of the simplifier
    1.10 +  can be restored like this:  declare/using [[simp_legacy_precond]]
    1.11 +  This configuration option will disappear again in the future.
    1.12 +
    1.13  * HOL-Word:
    1.14    * Abandoned fact collection "word_arith_alts", which is a
    1.15    duplicate of "word_arith_wis".