author | paulson |
Tue, 10 Feb 1998 10:27:30 +0100 | |
changeset 4615 | 67457d16cdbc |
parent 4614 | 122015efd4e1 |
child 4616 | d257e6c6614f |
--- a/src/HOL/equalities.ML Tue Feb 10 10:26:58 1998 +0100 +++ b/src/HOL/equalities.ML Tue Feb 10 10:27:30 1998 +0100 @@ -319,6 +319,8 @@ by (Blast_tac 1); qed "Compl_INT"; +Addsimps [Compl_Un, Compl_Int, Compl_UN, Compl_INT]; + (*Halmos, Naive Set Theory, page 16.*) goal thy "((A Int B) Un C = A Int (B Un C)) = (C<=A)";