new theorem rev_ImageI
authorpaulson
Mon Jan 31 16:18:42 2000 +0100 (2000-01-31)
changeset 817456d9baa2ddb0
parent 8173 a9966d5ab84d
child 8175 7d08b047b76e
new theorem rev_ImageI
src/HOL/Relation.ML
     1.1 --- a/src/HOL/Relation.ML	Mon Jan 31 16:18:09 2000 +0100
     1.2 +++ b/src/HOL/Relation.ML	Mon Jan 31 16:18:42 2000 +0100
     1.3 @@ -341,6 +341,11 @@
     1.4  AddIs  [ImageI];
     1.5  AddSEs [ImageE];
     1.6  
     1.7 +(*This version's more effective when we already have the required "a"*)
     1.8 +Goal  "[| a:A;  (a,b): r |] ==> b : r^^A";
     1.9 +by (Blast_tac 1);
    1.10 +qed "rev_ImageI";
    1.11 +
    1.12  
    1.13  Goal "R^^{} = {}";
    1.14  by (Blast_tac 1);