NEWS

   finite_choice ~> finite_set_choice
   eventually_conjI ~> eventually_conj
   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]
   Lim_neg ~> tendsto_minus
   Lim_add ~> tendsto_add