--- 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)";