# HG changeset patch
# User paulson
# Date 835968579 -7200
# Node ID a6d7aef48c2f7c58878939edc8967ee5229377ae
# Parent  a9c36056d320ae1be67d6fe8f3abead06f677394
Removed the unused eq_cs, and added some distributive laws

diff -r a9c36056d320 -r a6d7aef48c2f src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri Jun 28 15:29:05 1996 +0200
+++ b/src/HOL/equalities.ML	Fri Jun 28 15:29:39 1996 +0200
@@ -10,8 +10,6 @@
 
 AddSIs [equalityI];
 
-val eq_cs = set_cs addSIs [equalityI];
-
 section "{}";
 
 goal Set.thy "{x.False} = {}";
@@ -71,6 +69,15 @@
 by (Fast_tac 1);
 qed "mk_disjoint_insert";
 
+goal Set.thy
+    "!!A. A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
+by (Fast_tac 1);
+qed "UN_insert_distrib";
+
+goal Set.thy "(UN x. insert a (B x)) = insert a (UN x. B x)";
+by (Fast_tac 1);
+qed "UN1_insert_distrib";
+
 section "``";
 
 goal Set.thy "f``{} = {}";
@@ -192,7 +199,7 @@
 qed "Un_UNIV_right";
 Addsimps[Un_UNIV_right];
 
-goal Set.thy "insert a B Un C = insert a (B Un C)";
+goal Set.thy "(insert a B) Un C = insert a (B Un C)";
 by (Fast_tac 1);
 qed "Un_insert_left";