changeset 44907 | 93943da0a010 |
parent 44904 | 2ba4174f1e7d |
child 44908 | f05bff62f8a6 |
--- a/NEWS Mon Sep 12 11:39:29 2011 -0700 +++ b/NEWS Mon Sep 12 11:54:20 2011 -0700 @@ -294,6 +294,7 @@ eventually_and ~> eventually_conj_iff eventually_false ~> eventually_False setsum_norm ~> norm_setsum + Lim_sequentially ~> LIMSEQ_def Lim_ident_at ~> LIM_ident Lim_const ~> tendsto_const Lim_cmul ~> tendsto_scaleR [OF tendsto_const]