src/HOL/Vimage.ML
changeset 7516 a1d476251238
parent 7031 972b5f62f476
child 7823 742715638a01
--- a/src/HOL/Vimage.ML	Wed Sep 08 15:38:54 1999 +0200
+++ b/src/HOL/Vimage.ML	Wed Sep 08 15:39:52 1999 +0200
@@ -43,11 +43,6 @@
 
 (*** Simple equalities ***)
 
-Goal "(%x. x) -`` B = B";
-by (Blast_tac 1);
-qed "ident_vimage";
-Addsimps [ident_vimage];
-
 Goal "f-``{} = {}";
 by (Blast_tac 1);
 qed "vimage_empty";