# HG changeset patch
# User paulson
# Date 943352299 -3600
# Node ID 61dde9078e245dcdd9d6e98fb4731c6b43fba98d
# Parent  199721f2eb2d3d770d55a3495a78c603b4b24cb8
new theorem rev_image_eqI

diff -r 199721f2eb2d -r 61dde9078e24 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Mon Nov 22 12:10:27 1999 +0100
+++ b/src/HOL/Set.ML	Tue Nov 23 11:18:19 1999 +0100
@@ -650,6 +650,11 @@
 
 bind_thm ("imageI", refl RS image_eqI);
 
+(*This version's more effective when we already have the required x*)
+Goalw [image_def] "[| x:A;  b=f(x) |] ==> b : f``A";
+by (Blast_tac 1);
+qed "rev_image_eqI";
+
 (*The eta-expansion gives variable-name preservation.*)
 val major::prems = Goalw [image_def]
     "[| b : (%x. f(x))``A;  !!x.[| b=f(x);  x:A |] ==> P |] ==> P";