# HG changeset patch
# User paulson
# Date 889091247 -3600
# Node ID c9d3524282017025802f979211f2ca2d8ed09d01
# Parent  24917efb31b5b0ef9c988d59f388ed1541273973
New theorem and simprules

diff -r 24917efb31b5 -r c9d352428201 src/HOL/Vimage.ML
--- 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";