# HG changeset patch # User wenzelm # Date 1530305435 -7200 # Node ID a22540ac70528dfc8c1b1cb7f2fb88d1b2d69d7b # Parent 549a4992222f71f7cf7f8777cd50199ae5cadfca tuned; diff -r 549a4992222f -r a22540ac7052 CONTRIBUTORS --- a/CONTRIBUTORS Fri Jun 29 22:14:33 2018 +0200 +++ b/CONTRIBUTORS Fri Jun 29 22:50:35 2018 +0200 @@ -42,7 +42,8 @@ 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. + 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 diff -r 549a4992222f -r a22540ac7052 NEWS --- a/NEWS Fri Jun 29 22:14:33 2018 +0200 +++ b/NEWS Fri Jun 29 22:50:35 2018 +0200 @@ -399,8 +399,8 @@ as 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. +* 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