src/HOL/Library/Formal_Power_Series.thy
changeset 60017 b785d6d06430
parent 59867 58043346ca64
child 60162 645058aa9d6f
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -624,7 +624,7 @@
     1.4        by blast
     1.5    }
     1.6    then show ?thesis
     1.7 -    unfolding LIMSEQ_def by blast
     1.8 +    unfolding lim_sequentially by blast
     1.9  qed
    1.10  
    1.11