NEWS
changeset 58776 95e58e04e534
parent 58775 9cd64a66a765
child 58785 e7d2b46520e0
     1.1 --- a/NEWS	Fri Oct 24 15:07:49 2014 +0200
     1.2 +++ b/NEWS	Fri Oct 24 15:07:51 2014 +0200
     1.3 @@ -65,6 +65,12 @@
     1.4  * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
     1.5  Minor INCOMPATIBILITY.
     1.6  
     1.7 +* field_simps: Use NO_MATCH-simproc for distribution rules, to avoid
     1.8 +  non-termination in case of distributing a division. With this change
     1.9 +  field_simps is in some cases slightly less powerful, if it fails try
    1.10 +  to add algebra_simps, or use divide_simps.
    1.11 +Minor INCOMPATIBILITY.
    1.12 +
    1.13  * Bootstrap of listsum as special case of abstract product over lists.
    1.14  Fact rename:
    1.15      listsum_def ~> listsum.eq_foldr