--- a/src/HOL/Sum.ML Tue Jul 25 16:58:06 1995 +0200
+++ b/src/HOL/Sum.ML Tue Jul 25 16:59:08 1995 +0200
@@ -202,3 +202,11 @@
by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
qed "Part_id";
+goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
+by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+qed "Part_Int";
+
+(*For inductive definitions*)
+goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
+by (fast_tac (set_cs addIs [PartI,equalityI] addSEs [PartE]) 1);
+qed "Part_Collect";