# HG changeset patch
# User oheimb
# Date 894054463 -7200
# Node ID 379314255a04e24836ea4980623320481f586b53
# Parent  d80faf83c82f4e65072a9e71dc4f5b1423c596e2
added insert_Collect

diff -r d80faf83c82f -r 379314255a04 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Fri May 01 19:51:03 1998 +0200
+++ b/src/HOL/equalities.ML	Fri May 01 22:27:43 1998 +0200
@@ -82,6 +82,9 @@
 by (Blast_tac 1);
 qed "mk_disjoint_insert";
 
+bind_thm ("insert_Collect", prove_goal thy 
+	"insert a (Collect P) = {u. u ~= a --> P u}" (K [Auto_tac]));
+
 goal thy
     "!!A. A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
 by (Blast_tac 1);