# HG changeset patch # User eberlm # Date 1500125790 -3600 # Node ID 978fb83b100c17682d1151495b0f5aa286fe9116 # Parent 512b0dc09061033732de537dd55153c0ad351558 Updated NEWS diff -r 512b0dc09061 -r 978fb83b100c NEWS --- a/NEWS Sat Jul 15 14:33:56 2017 +0100 +++ b/NEWS Sat Jul 15 14:36:30 2017 +0100 @@ -105,6 +105,11 @@ *** HOL *** +* Notions of squarefreeness, n-th powers, and prime powers in +HOL-Computational_Algebra and HOL-Number_Theory. + +* Material on infinite products in HOL-Analysis + * "sublist" from theory List renamed to "nths" in analogy with "nth". "sublisteq" renamed to "subseq". Minor INCOMPATIBILITY.