src/ZF/equalities.ML
changeset 520 806d3f00590d
parent 517 a9f93400f307
child 536 5fbfa997f1b0
--- 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();