src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Fri Nov 12 20:55:04 2004 +0100
+++ b/src/HOL/Finite_Set.thy	Sat Nov 13 07:47:34 2004 +0100
@@ -123,6 +123,10 @@
   apply (simp only: finite_Un, blast)
   done
 
+lemma finite_Union[simp, intro]:
+ "\<lbrakk> finite A; !!M. M \<in> A \<Longrightarrow> finite M \<rbrakk> \<Longrightarrow> finite(\<Union>A)"
+by (induct rule:finite_induct) simp_all
+
 lemma finite_empty_induct:
   "finite A ==>
   P A ==> (!!a A. finite A ==> a:A ==> P A ==> P (A - {a})) ==> P {}"