src/HOL/equalities.ML
changeset 1843 a6d7aef48c2f
parent 1786 8a31d85d27b8
child 1879 83c70ad381c1
     1.1 --- a/src/HOL/equalities.ML	Fri Jun 28 15:29:05 1996 +0200
     1.2 +++ b/src/HOL/equalities.ML	Fri Jun 28 15:29:39 1996 +0200
     1.3 @@ -10,8 +10,6 @@
     1.4  
     1.5  AddSIs [equalityI];
     1.6  
     1.7 -val eq_cs = set_cs addSIs [equalityI];
     1.8 -
     1.9  section "{}";
    1.10  
    1.11  goal Set.thy "{x.False} = {}";
    1.12 @@ -71,6 +69,15 @@
    1.13  by (Fast_tac 1);
    1.14  qed "mk_disjoint_insert";
    1.15  
    1.16 +goal Set.thy
    1.17 +    "!!A. A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
    1.18 +by (Fast_tac 1);
    1.19 +qed "UN_insert_distrib";
    1.20 +
    1.21 +goal Set.thy "(UN x. insert a (B x)) = insert a (UN x. B x)";
    1.22 +by (Fast_tac 1);
    1.23 +qed "UN1_insert_distrib";
    1.24 +
    1.25  section "``";
    1.26  
    1.27  goal Set.thy "f``{} = {}";
    1.28 @@ -192,7 +199,7 @@
    1.29  qed "Un_UNIV_right";
    1.30  Addsimps[Un_UNIV_right];
    1.31  
    1.32 -goal Set.thy "insert a B Un C = insert a (B Un C)";
    1.33 +goal Set.thy "(insert a B) Un C = insert a (B Un C)";
    1.34  by (Fast_tac 1);
    1.35  qed "Un_insert_left";
    1.36