src/HOL/Library/Liminf_Limsup.thy
changeset 61806 d2e62ae01cd8
parent 61730 2b775b888897
child 61810 3c5040d5694a
--- a/src/HOL/Library/Liminf_Limsup.thy	Mon Dec 07 10:38:04 2015 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy	Mon Dec 07 16:44:26 2015 +0000
@@ -100,7 +100,7 @@
 lemma Liminf_eq:
   assumes "eventually (\<lambda>x. f x = g x) F"
   shows "Liminf F f = Liminf F g"
-  by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
+  by (intro antisym Liminf_mono eventually_mono'[OF assms]) auto
 
 lemma Limsup_mono:
   assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
@@ -116,7 +116,7 @@
 lemma Limsup_eq:
   assumes "eventually (\<lambda>x. f x = g x) net"
   shows "Limsup net f = Limsup net g"
-  by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
+  by (intro antisym Limsup_mono eventually_mono'[OF assms]) auto
 
 lemma Liminf_le_Limsup:
   assumes ntriv: "\<not> trivial_limit F"