changeset 8993 | cbfebff56cc0 |
parent 8333 | 226d12ac76e2 |
child 9077 | 5bf9b0d6df8a |
--- 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";