New lemmas involving Int

--- a/src/HOL/Finite.ML	Tue Sep 01 10:11:06 1998 +0200
+++ b/src/HOL/Finite.ML	Tue Sep 01 10:25:05 1998 +0200
@@ -56,11 +56,23 @@
 
 Goal "finite(F Un G) = (finite F & finite G)";
 by (blast_tac (claset() 
-	         addIs [read_instantiate [("B", "?AA Un ?BB")] finite_subset, 
+	         addIs [read_instantiate [("B", "?X Un ?Y")] finite_subset, 
 			finite_UnI]) 1);
 qed "finite_Un";
 AddIffs[finite_Un];
 
+Goal "finite F ==> finite(F Int G)";
+by (blast_tac (claset() addIs [finite_subset]) 1);
+qed "finite_Int1";
+
+Goal "finite G ==> finite(F Int G)";
+by (blast_tac (claset() addIs [finite_subset]) 1);
+qed "finite_Int2";
+
+Addsimps[finite_Int1, finite_Int2];
+AddIs[finite_Int1, finite_Int2];
+
+
 Goal "finite(insert a A) = finite A";
 by (stac insert_is_Un 1);
 by (simp_tac (HOL_ss addsimps [finite_Un]) 1);