ZF/equalities/Sigma_cons: new
ZF/equalities/cons_eq: new
ZF/equalities.thy: added final newline

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

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