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