src/HOL/Library/Infinite_Set.thy

--- a/src/HOL/Library/Infinite_Set.thy	Fri Mar 19 06:14:37 2010 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Sat Mar 20 02:23:41 2010 +0100
@@ -52,6 +52,9 @@
 lemma Un_infinite: "infinite S \<Longrightarrow> infinite (S \<union> T)"
   by simp
 
+lemma infinite_Un: "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
+  by simp
+
 lemma infinite_super:
   assumes T: "S \<subseteq> T" and S: "infinite S"
   shows "infinite T"