--- a/src/HOL/Library/Extended_Real.thy Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy Mon Apr 25 16:09:26 2016 +0200
@@ -3900,7 +3900,7 @@
shows Liminf_inverse_ereal: "Liminf F (\<lambda>x. inverse (f x)) = inverse (Limsup F f)"
and Limsup_inverse_ereal: "Limsup F (\<lambda>x. inverse (f x)) = inverse (Liminf F f)"
proof -
- def inv \<equiv> "\<lambda>x. if x \<le> 0 then \<infinity> else inverse x :: ereal"
+ define inv where [abs_def]: "inv x = (if x \<le> 0 then \<infinity> else inverse x)" for x :: ereal
have "continuous_on ({..0} \<union> {0..}) inv" unfolding inv_def
by (intro continuous_on_If) (auto intro!: continuous_intros)
also have "{..0} \<union> {0..} = (UNIV :: ereal set)" by auto