# HG changeset patch
# User wenzelm
# Date 959543909 -7200
# Node ID cbfebff56cc0f7935ac6fe3f6a80ec577d6eec92
# Parent  6addcdd363b7b4026b38d2330ca7c53bb739faac
Collect_neg_eq;

diff -r 6addcdd363b7 -r cbfebff56cc0 src/HOL/equalities.ML
--- 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";