diff -r 06e195515deb -r 87429bdecad5 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Mon Jun 30 15:45:03 2014 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Mon Jun 30 15:45:21 2014 +0200
@@ -80,6 +80,12 @@
 lemmas ereal2_cases = ereal_cases[case_product ereal_cases]
 lemmas ereal3_cases = ereal2_cases[case_product ereal_cases]
 
+lemma ereal_all_split: "\<And>P. (\<forall>x::ereal. P x) \<longleftrightarrow> P \<infinity> \<and> (\<forall>x. P (ereal x)) \<and> P (-\<infinity>)"
+  by (metis ereal_cases)
+
+lemma ereal_ex_split: "\<And>P. (\<exists>x::ereal. P x) \<longleftrightarrow> P \<infinity> \<or> (\<exists>x. P (ereal x)) \<or> P (-\<infinity>)"
+  by (metis ereal_cases)
+
 lemma ereal_uminus_eq_iff[simp]:
   fixes a b :: ereal
   shows "-a = -b \<longleftrightarrow> a = b"
@@ -2121,7 +2127,6 @@
     by auto
 qed
 
-
 subsubsection {* Convergent sequences *}
 
 lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"