# HG changeset patch
# User paulson
# Date 939809285 -7200
# Node ID 3561e0da35b8a38380d92c43e0d80bd02f4b29b2
# Parent  6462cb4dfdc202a0d42d914c714a5eb747c623a6
more Collect laws

diff -r 6462cb4dfdc2 -r 3561e0da35b8 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Wed Oct 13 12:07:44 1999 +0200
+++ b/src/HOL/equalities.ML	Wed Oct 13 12:08:05 1999 +0200
@@ -36,6 +36,22 @@
 by (Blast_tac 1);
 qed "Collect_conj_eq";
 
+Goal "{x. ALL y. P x y} = (INT y. {x. P x y})";
+by (Blast_tac 1);
+qed "Collect_all_eq";
+
+Goal "{x. ALL y: A. P x y} = (INT y: A. {x. P x y})";
+by (Blast_tac 1);
+qed "Collect_ball_eq";
+
+Goal "{x. EX y. P x y} = (UN y. {x. P x y})";
+by (Blast_tac 1);
+qed "Collect_ex_eq";
+
+Goal "{x. EX y: A. P x y} = (UN y: A. {x. P x y})";
+by (Blast_tac 1);
+qed "Collect_bex_eq";
+
 
 section "insert";