--- a/src/HOL/Vimage.ML Wed Mar 04 13:16:05 1998 +0100
+++ b/src/HOL/Vimage.ML Thu Mar 05 10:47:27 1998 +0100
@@ -14,6 +14,8 @@
"(a : f-``B) = (f a : B)"
(fn _ => [ (Blast_tac 1) ]);
+Addsimps [vimage_eq];
+
qed_goal "vimage_singleton_eq" thy
"(a : f-``{b}) = (f a = b)"
(fn _ => [ simp_tac (simpset() addsimps [vimage_eq]) 1 ]);
@@ -34,6 +36,11 @@
(*** Simple equalities ***)
+goal thy "(%x. x) -`` B = B";
+by (Blast_tac 1);
+qed "ident_vimage";
+Addsimps [ident_vimage];
+
goal thy "f-``{} = {}";
by (Blast_tac 1);
qed "vimage_empty";