changeset 44538 | 8037d25afa89 |
parent 44531 | 1d477a2b1572 |
child 44568 | e6f291cb5810 |
--- 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]