NEWS
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.