changeset 58321 | 44692d31a399 |
parent 58310 | 91ea607a34d8 |
child 58368 | fe083c681ed8 |
--- 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.