src/HOL/equalities.ML
changeset 1564 822575c737bd
parent 1553 4eb4a9c7d736
child 1618 372880456b5b
     1.1 --- a/src/HOL/equalities.ML	Mon Mar 11 14:08:09 1996 +0100
     1.2 +++ b/src/HOL/equalities.ML	Mon Mar 11 14:09:50 1996 +0100
     1.3 @@ -277,12 +277,9 @@
     1.4  qed "Inter_insert";
     1.5  Addsimps[Inter_insert];
     1.6  
     1.7 -(* Why does fast_tac fail???
     1.8 -goal Set.thy "Inter(A Int B) = Inter(A) Int Inter(B)";
     1.9 -by (fast_tac eq_cs 1);
    1.10 -qed "Inter_Int_distrib";
    1.11 -Addsimps[Inter_Int_distrib];
    1.12 -*)
    1.13 +goal Set.thy "Inter(A) Un Inter(B) <= Inter(A Int B)";
    1.14 +by (fast_tac set_cs 1);
    1.15 +qed "Inter_Un_subset";
    1.16  
    1.17  goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
    1.18  by (best_tac eq_cs 1);