# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1661462329 -3600
# Node ID 44e0ba464e087ae7f90eff5274f8ef9374198425
# Parent  c2dc1102b7765d25145b3126fc49a22bc9c505a3
NEWS about Sum_of_Powers

diff -r c2dc1102b776 -r 44e0ba464e08 NEWS
--- a/NEWS	Thu Aug 25 21:42:21 2022 +0100
+++ b/NEWS	Thu Aug 25 22:18:49 2022 +0100
@@ -155,6 +155,9 @@
 * Theory "HOL-Library.Sublist":
   - Added lemma map_mono_strict_suffix.
 
+* Theory "HOL-ex.Sum_of_Powers":
+  - Deleted. The same material is in the AFP as Bernoulli.
+
 * Nitpick: To avoid technical issues, prefer non-JNI solvers to JNI solvers by
   default. Minor INCOMPATIBILITY.