# HG changeset patch
# User lcp
# Date 806684348 -7200
# Node ID 0443e4dc8511b37e0d82a7953ce4efd25f3c097f
# Parent  bc94f00e47ba0c3576054b6ca3b35930054f8047
Added Part_Int and Part_Collect for inductive definitions

diff -r bc94f00e47ba -r 0443e4dc8511 src/HOL/Sum.ML
--- 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";