changeset 62390 | 842917225d56 |
parent 62175 | 8ffc4d0e652d |
child 62393 | a620a8756b7c |
--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Tue Feb 23 16:25:08 2016 +0100 @@ -509,4 +509,4 @@ unfolding uniformly_convergent_on_def by (blast dest: bounded_linear_uniform_limit_intros(13)) -end \ No newline at end of file +end