src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
changeset 60017 b785d6d06430
parent 59865 8a20dd967385
child 60420 884f54e01427
     1.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -188,7 +188,7 @@
     1.4        by simp
     1.5    qed
     1.6    show "convergent f"
     1.7 -  proof (rule convergentI, subst LIMSEQ_def, safe)
     1.8 +  proof (rule convergentI, subst lim_sequentially, safe)
     1.9      --{* The limit function converges according to its norm *}
    1.10      fix e::real
    1.11      assume "e > 0" hence "e/2 > 0" by simp