# HG changeset patch
# User paulson
# Date 887102850 -3600
# Node ID 67457d16cdbc478898e9f95c612f1ccb586af9b9
# Parent  122015efd4e1e8a32659be5ad473f8d804185d40
New Addsimps for Compl rules

diff -r 122015efd4e1 -r 67457d16cdbc src/HOL/equalities.ML
--- 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)";