# HG changeset patch
# User paulson
# Date 949331922 -3600
# Node ID 56d9baa2ddb022437f5393447f6938a99b8483c8
# Parent  a9966d5ab84d4bee227961a8a8ab3424a20dc184
new theorem rev_ImageI

diff -r a9966d5ab84d -r 56d9baa2ddb0 src/HOL/Relation.ML
--- 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);