# HG changeset patch # User paulson # Date 947780944 -3600 # Node ID 4a53041acb281fe737b581ae4521d8ec5d353d50 # Parent 0b383485564340b97eb7d583fa06669fafc449a9 new theorem subset_Compl_self_eq diff -r 0b3834855643 -r 4a53041acb28 src/HOL/equalities.ML --- a/src/HOL/equalities.ML Thu Jan 13 15:29:52 2000 +0100 +++ b/src/HOL/equalities.ML Thu Jan 13 17:29:04 2000 +0100 @@ -401,8 +401,11 @@ Addsimps [Compl_Un, Compl_Int, Compl_UN, Compl_INT]; +Goal "(A <= -A) = (A = {})"; +by (Blast_tac 1); +qed "subset_Compl_self_eq"; + (*Halmos, Naive Set Theory, page 16.*) - Goal "((A Int B) Un C = A Int (B Un C)) = (C<=A)"; by (blast_tac (claset() addSEs [equalityCE]) 1); qed "Un_Int_assoc_eq";