--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Mon Dec 07 16:44:26 2015 +0000
@@ -477,9 +477,7 @@
lemma uniform_limit_on_subset:
"uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
- by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_rev_mono)
-
-
+ by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono')
lemma uniformly_convergent_add:
"uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>