| changeset 9447 | e5180c869772 |
| parent 9422 | 4b6bc2b347e5 |
| child 9608 | a50dcf0475ad |
--- a/src/HOL/equalities.ML Tue Jul 25 23:33:13 2000 +0200 +++ b/src/HOL/equalities.ML Wed Jul 26 19:42:19 2000 +0200 @@ -425,6 +425,16 @@ Addsimps [Compl_UNIV_eq, Compl_empty_eq]; +Goal "(-A <= -B) = (B <= (A::'a set))"; +by(Blast_tac 1); +qed "Compl_subset_Compl_iff"; +AddIffs [Compl_subset_Compl_iff]; + +Goal "(-A = -B) = (A = (B::'a set))"; +by(Blast_tac 1); +qed "Compl_eq_Compl_iff"; +AddIffs [Compl_eq_Compl_iff]; + section "Union";