author | haftmann |
Fri, 12 Sep 2014 07:38:15 +0200 | |
changeset 58321 | 44692d31a399 |
parent 58320 | 351810c45a48 |
child 58323 | 29b8688c5f76 |
--- a/NEWS Thu Sep 11 23:12:32 2014 +0200 +++ b/NEWS Fri Sep 12 07:38:15 2014 +0200 @@ -23,6 +23,11 @@ *** HOL *** +* Bootstrap of listsum as special case of abstract product over lists. +Fact rename: + listsum_def ~> listsum.eq_foldr +INCOMPATIBILITY. + * Command and antiquotation "value" provide different evaluation slots (again), where the previous strategy (nbe after ML) serves as default. Minor INCOMPATIBILITY.