# HG changeset patch
# User lcp
# Date 776966823 -7200
# Node ID 806d3f00590d3e965302961ddd9d292688eb645e
# Parent  98b88551e10251f310841ff5da5f67b4e4a210ef
ZF/equalities/Sigma_cons: new
ZF/equalities/cons_eq: new
ZF/equalities.thy: added final newline

diff -r 98b88551e102 -r 806d3f00590d src/ZF/equalities.ML
--- a/src/ZF/equalities.ML	Mon Aug 15 18:04:10 1994 +0200
+++ b/src/ZF/equalities.ML	Mon Aug 15 18:07:03 1994 +0200
@@ -9,6 +9,11 @@
 
 (** Finite Sets **)
 
+(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*)
+goal ZF.thy "{a} Un B = cons(a,B)";
+by (fast_tac eq_cs 1);
+val cons_eq = result();
+
 goal ZF.thy "cons(a, cons(b, C)) = cons(b, cons(a, C))";
 by (fast_tac eq_cs 1);
 val cons_commute = result();
@@ -257,6 +262,10 @@
 
 (** Unions and Intersections with General Sum **)
 
+goal ZF.thy "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)";
+by (fast_tac eq_cs 1);
+val Sigma_cons = result();
+
 goal ZF.thy "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))";
 by (fast_tac eq_cs 1);
 val SUM_UN_distrib1 = result();
diff -r 98b88551e102 -r 806d3f00590d src/ZF/equalities.thy
--- a/src/ZF/equalities.thy	Mon Aug 15 18:04:10 1994 +0200
+++ b/src/ZF/equalities.thy	Mon Aug 15 18:07:03 1994 +0200
@@ -1,3 +1,3 @@
 (*Dummy theory to document dependencies *)
 
-equalities = "domrange"
\ No newline at end of file
+equalities = "domrange"