# HG changeset patch
# User nipkow
# Date 1128461446 -7200
# Node ID 2c42d0a94f58ce1512d52242dbf846cd0cd428f7
# Parent  4191beda8b90e6cf24cec1b93beb199c61e8c1dd
new lemmas

diff -r 4191beda8b90 -r 2c42d0a94f58 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Oct 04 21:39:16 2005 +0200
+++ b/src/HOL/Finite_Set.thy	Tue Oct 04 23:30:46 2005 +0200
@@ -177,6 +177,9 @@
   qed
 qed
 
+lemma finite_Collect_subset: "finite A \<Longrightarrow> finite{x \<in> A. P x}"
+using finite_subset[of "{x \<in> A. P x}" "A"] by blast
+
 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
   by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)