changeset 44710 | 9caf6883f1f4 |
parent 44681 | 49ef76b4a634 |
child 44711 | cd8dbfc272df |
--- a/NEWS Sun Sep 04 07:15:13 2011 -0700 +++ b/NEWS Sun Sep 04 09:49:45 2011 -0700 @@ -296,6 +296,9 @@ LIMSEQ_norm_zero ~> tendsto_norm_zero_iff LIMSEQ_rabs_zero ~> tendsto_rabs_zero_iff LIMSEQ_imp_rabs ~> tendsto_rabs + LIMSEQ_add_minus ~> tendsto_add [OF _ tendsto_minus] + LIMSEQ_add_const ~> tendsto_add [OF _ tendsto_const] + LIMSEQ_diff_const ~> tendsto_diff [OF _ tendsto_const] LIM_ident ~> tendsto_ident_at LIM_const ~> tendsto_const LIM_add ~> tendsto_add