author | huffman |
Fri, 26 Aug 2011 15:11:26 -0700 | |
changeset 44538 | 8037d25afa89 |
parent 44537 | c10485a6a7af |
child 44539 | ddfd934e19bb |
--- 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]