--- a/src/HOL/equalities.ML Wed Oct 27 19:29:47 1999 +0200
+++ b/src/HOL/equalities.ML Wed Oct 27 19:32:19 1999 +0200
@@ -28,6 +28,11 @@
qed "not_psubset_empty";
AddIffs [not_psubset_empty];
+Goal "(Collect P = {}) = (!x. ~ P x)";
+by Auto_tac;
+qed "Collect_empty_eq";
+Addsimps[Collect_empty_eq];
+
Goal "{x. P x | Q x} = {x. P x} Un {x. Q x}";
by (Blast_tac 1);
qed "Collect_disj_eq";
@@ -153,6 +158,14 @@
qed "image_cong";
+section "range";
+
+Goal "{u. ? x. u = f x} = range f";
+by Auto_tac;
+qed "full_SetCompr_eq";
+Addsimps[full_SetCompr_eq];
+
+
section "Int";
Goal "A Int A = A";