--- a/CONTRIBUTORS Fri Jun 29 10:24:36 2018 +0200
+++ b/CONTRIBUTORS Fri Jun 29 10:55:05 2018 +0100
@@ -34,6 +34,9 @@
* March 2018: Viorel Preoteasa
Generalisation of complete_distrib_lattice
+* February 2018: Wenda Li
+ A unified definition for the order of zeros and poles. Improved reasoning around non-essential singularities.
+
* January 2018: Sebastien Gouezel
Various small additions to HOL-Analysis
--- a/NEWS Fri Jun 29 10:24:36 2018 +0200
+++ b/NEWS Fri Jun 29 10:55:05 2018 +0100
@@ -390,6 +390,10 @@
Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi.
INCOMPATIBILITY.
+* Session HOL-Analysis: the functions zorder, zer_poly, porder and pol_poly have been redefined.
+All related lemmas have been reworked.
+INCOMPATIBILITY.
+
* Session HOL-Analysis: infinite products, Moebius functions, the
Riemann mapping theorem, the Vitali covering theorem,
change-of-variables results for integration and measures.