# HG changeset patch
# User paulson
# Date 929608463 -7200
# Node ID 0c92ccb3c4ba968490424f4840064e7d65c9937d
# Parent  799859f2e65763e109758c72ee4bf1949f00db81
moved image_UNION to Fun/image_UN

diff -r 799859f2e657 -r 0c92ccb3c4ba src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Thu Jun 17 10:33:43 1999 +0200
+++ b/src/HOL/equalities.ML	Thu Jun 17 10:34:23 1999 +0200
@@ -54,8 +54,8 @@
 Goal "a:A ==> insert a A = A";
 by (Blast_tac 1);
 qed "insert_absorb";
-(* Addsimps [insert_absorb] causes recursive (ie quadtratic) calls
-   in case of nested inserts!
+(* Addsimps [insert_absorb] causes recursive calls
+   when there are nested inserts, with QUADRATIC running time
 *)
 
 Goal "insert x (insert x A) = insert x A";
@@ -101,11 +101,6 @@
 qed "image_insert";
 Addsimps[image_insert];
 
-(*image_INTER fails, perhaps even if f is injective*)
-Goal  "(f `` (UNION A B)) = (UN x:A.(f `` (B x)))";
-by (Blast_tac 1);
-qed "image_UNION";
-
 Goal "(%x. x) `` Y = Y";
 by (Blast_tac 1);
 qed "image_id";