# HG changeset patch
# User lcp
# Date 776966977 -7200
# Node ID dfca17a698b01a8c26a11766a64dde355aa029f6
# Parent  806d3f00590d3e965302961ddd9d292688eb645e
ZF/Sum/Sigma_bool: new

diff -r 806d3f00590d -r dfca17a698b0 src/ZF/Sum.ML
--- a/src/ZF/Sum.ML	Mon Aug 15 18:07:03 1994 +0200
+++ b/src/ZF/Sum.ML	Mon Aug 15 18:09:37 1994 +0200
@@ -10,6 +10,10 @@
 
 val sum_defs = [sum_def,Inl_def,Inr_def,case_def];
 
+goalw Sum.thy (bool_def::sum_defs) "Sigma(bool,C) = C(0) + C(1)";
+by (fast_tac eq_cs 1);
+val Sigma_bool = result();
+
 (** Introduction rules for the injections **)
 
 goalw Sum.thy sum_defs "!!a A B. a : A ==> Inl(a) : A+B";
@@ -84,6 +88,7 @@
 by (fast_tac ZF_cs 1);
 val sum_equal_iff = result();
 
+
 (*** Eliminator -- case ***)
 
 goalw Sum.thy sum_defs "case(c, d, Inl(a)) = c(a)";