diff -r db33de6cb570 -r c6849a634582 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Fri Mar 19 12:24:16 2010 +0100
+++ b/Nominal/Abs.thy	Fri Mar 19 12:28:35 2010 +0100
@@ -782,5 +782,10 @@
   \<and> pi \<bullet> bs = cs)"
 by (simp add: alpha_gen)
 
+(* maybe should be added to Infinite.thy *)
+lemma infinite_Un:
+  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
+  by simp
+
 end