diff -r fa5b67fb70ad -r af9eb5e566dd src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Sat Oct 25 19:20:28 2014 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Sun Oct 26 19:11:16 2014 +0100
@@ -1232,9 +1232,8 @@
 lemma ereal_power_divide:
   fixes x y :: ereal
   shows "y \<noteq> 0 \<Longrightarrow> (x / y) ^ n = x^n / y^n"
-  by (cases rule: ereal2_cases[of x y])
-     (auto simp: one_ereal_def zero_ereal_def power_divide not_le
-                 power_less_zero_eq zero_le_power_iff)
+  by (cases rule: ereal2_cases [of x y])
+     (auto simp: one_ereal_def zero_ereal_def power_divide zero_le_power_eq)
 
 lemma ereal_le_mult_one_interval:
   fixes x y :: ereal