Collect_neg_eq;

--- a/src/HOL/equalities.ML	Sun May 28 21:57:40 2000 +0200
+++ b/src/HOL/equalities.ML	Sun May 28 21:58:29 2000 +0200
@@ -33,6 +33,10 @@
 qed "Collect_empty_eq";
 Addsimps[Collect_empty_eq];
 
+Goal "{x. ~ (P x)} = - {x. P x}";
+by (Blast_tac 1);
+qed "Collect_neg_eq";
+
 Goal "{x. P x | Q x} = {x. P x} Un {x. Q x}";
 by (Blast_tac 1);
 qed "Collect_disj_eq";