--- a/src/HOL/Analysis/Uniform_Limit.thy Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy Thu Feb 22 15:17:25 2018 +0100
@@ -438,6 +438,7 @@
bounded_linear.uniform_limit[OF bounded_linear_mult_right]
bounded_linear.uniform_limit[OF bounded_linear_scaleR_left]
+
lemmas uniform_limit_uminus[uniform_limit_intros] =
bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]
@@ -728,5 +729,7 @@
apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
using sm sums_unique by fastforce
+lemmas uniform_limit_subset_union = uniform_limit_on_subset[OF uniform_limit_on_Union]
+
end