# HG changeset patch # User huffman # Date 1314396686 25200 # Node ID 8037d25afa893781b3e51c6ffdb57360094368f4 # Parent c10485a6a7af5a0da275bd9c8754aeef33f8df1a NEWS entry for setsum_norm ~> norm_setsum diff -r c10485a6a7af -r 8037d25afa89 NEWS --- a/NEWS Fri Aug 26 15:00:00 2011 -0700 +++ b/NEWS Fri Aug 26 15:11:26 2011 -0700 @@ -206,6 +206,7 @@ eventually_conjI ~> eventually_conj eventually_and ~> eventually_conj_iff eventually_false ~> eventually_False + setsum_norm ~> norm_setsum Lim_ident_at ~> LIM_ident Lim_const ~> tendsto_const Lim_cmul ~> tendsto_scaleR [OF tendsto_const]