# HG changeset patch
# User lcp
# Date 786901378 -3600
# Node ID 9f8bcf1a4cff7939227a52184124a90366e1ab2b
# Parent  5ca7f94117bbf3eaca601253d67f186af8578c57
sum_ss: moved down and added the rewrite rules for "case"

diff -r 5ca7f94117bb -r 9f8bcf1a4cff src/ZF/Sum.ML
--- a/src/ZF/Sum.ML	Thu Dec 08 16:07:12 1994 +0100
+++ b/src/ZF/Sum.ML	Thu Dec 08 16:42:58 1994 +0100
@@ -94,9 +94,6 @@
                    addSEs [PartE, sumE, Inl_neq_Inr, Inr_neq_Inl]
                    addSDs [Inl_inject, Inr_inject];
 
-val sum_ss = ZF_ss addsimps [InlI, InrI, Inl_iff, Inr_iff, 
-			     Inl_Inr_iff, Inr_Inl_iff];
-
 goal Sum.thy "!!A B. Inl(a): A+B ==> a: A";
 by (fast_tac sum_cs 1);
 qed "InlD";
@@ -154,6 +151,12 @@
 by (fast_tac sum_cs 1);
 qed "expand_case";
 
+val sum_ss = ZF_ss addsimps [InlI, InrI, Inl_iff, Inr_iff, 
+			     Inl_Inr_iff, Inr_Inl_iff,
+			     case_Inl, case_Inr];
+
+(*** More rules for Part(A,h) ***)
+
 goal Sum.thy "!!A B h. A<=B ==> Part(A,h)<=Part(B,h)";
 by (fast_tac sum_cs 1);
 qed "Part_mono";