new theorem rev_ImageI

--- a/src/HOL/Relation.ML	Mon Jan 31 16:18:09 2000 +0100
+++ b/src/HOL/Relation.ML	Mon Jan 31 16:18:42 2000 +0100
@@ -341,6 +341,11 @@
 AddIs  [ImageI];
 AddSEs [ImageE];
 
+(*This version's more effective when we already have the required "a"*)
+Goal  "[| a:A;  (a,b): r |] ==> b : r^^A";
+by (Blast_tac 1);
+qed "rev_ImageI";
+
 
 Goal "R^^{} = {}";
 by (Blast_tac 1);