# 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";