| changeset 4882 | 379314255a04 |
| parent 4771 | f1bacbbe02a8 |
| child 5069 | 3ea049f7979d |
--- 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);