# HG changeset patch
# User paulson
# Date 904637466 -7200
# Node ID 0c2472c74c2496e148c68567105a7a837d896029
# Parent  7a43b484f6d2e59adf446b862259a6118eb7e204
New lemmas involving Int

diff -r 7a43b484f6d2 -r 0c2472c74c24 src/ZF/Finite.ML
--- a/src/ZF/Finite.ML	Tue Sep 01 10:10:27 1998 +0200
+++ b/src/ZF/Finite.ML	Tue Sep 01 10:11:06 1998 +0200
@@ -48,6 +48,7 @@
 
 Addsimps [Fin_UnI];
 
+
 (*The union of a set of finite sets is finite.*)
 val [major] = goal Finite.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)";
 by (rtac (major RS Fin_induct) 1);
@@ -68,6 +69,18 @@
 by (REPEAT (ares_tac [Fin_subset_lemma RS spec RS mp] 1));
 qed "Fin_subset";
 
+Goal "b: Fin(A) ==> b Int c : Fin(A)";
+by (blast_tac (claset() addIs [Fin_subset]) 1);
+qed "Fin_IntI1";
+
+Goal "c: Fin(A) ==> b Int c : Fin(A)";
+by (blast_tac (claset() addIs [Fin_subset]) 1);
+qed "Fin_IntI2";
+
+Addsimps[Fin_IntI1, Fin_IntI2];
+AddIs[Fin_IntI1, Fin_IntI2];
+
+
 val major::prems = Goal
     "[| c: Fin(A);  b: Fin(A);                                  \
 \       P(b);                                                   \