| changeset 4615 | 67457d16cdbc |
| parent 4609 | b435c5a320b0 |
| child 4634 | 83d364462ce1 |
--- 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)";