NEWS
changeset 75976 c8d9fbe2dedd
parent 75973 3acc90a2ef6d
parent 75975 44e0ba464e08
child 75993 8f1bb89ddf4b
--- a/NEWS	Thu Aug 25 23:09:00 2022 +0200
+++ b/NEWS	Fri Aug 26 12:43:07 2022 +0100
@@ -163,6 +163,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.