src/HOL/Vimage.ML
changeset 5490 85855f65d0c6
parent 5143 b94cd208f073
child 7031 972b5f62f476
--- a/src/HOL/Vimage.ML	Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/Vimage.ML	Tue Sep 15 15:04:07 1998 +0200
@@ -53,7 +53,7 @@
 by (Blast_tac 1);
 qed "vimage_empty";
 
-Goal "f-``(Compl A) = Compl (f-``A)";
+Goal "f-``(-A) = -(f-``A)";
 by (Blast_tac 1);
 qed "vimage_Compl";