--- a/src/HOL/Library/Extended_Real.thy Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy Wed Mar 04 23:31:04 2015 +0100
@@ -2064,7 +2064,7 @@
by (cases m n rule: enat2_cases) auto
lemma numeral_le_ereal_of_enat_iff[simp]: "numeral m \<le> ereal_of_enat n \<longleftrightarrow> numeral m \<le> n"
- by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])
+by (cases n) (auto)
lemma numeral_less_ereal_of_enat_iff[simp]: "numeral m < ereal_of_enat n \<longleftrightarrow> numeral m < n"
by (cases n) auto