NEWS
authorhaftmann
Fri, 12 Sep 2014 07:38:15 +0200
changeset 58321 44692d31a399
parent 58320 351810c45a48
child 58323 29b8688c5f76
NEWS
NEWS
--- 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.