# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1269048221 -3600
# Node ID 65258d2c32147112384d120b6032bc11a9d96043
# Parent  23908b4dbc2fbd70f4cf1640a4a1dda83661a7ae
added lemma infinite_Un

diff -r 23908b4dbc2f -r 65258d2c3214 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"