1.1 --- a/src/HOL/Relation.thy	Mon Oct 26 23:27:16 2009 +0100
     1.2 +++ b/src/HOL/Relation.thy	Mon Oct 26 23:27:24 2009 +0100
     1.3 @@ -607,6 +607,9 @@
     1.4  lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
     1.5    by (auto simp:inv_image_def)
     1.6  
     1.7 +lemma converse_inv_image[simp]: "(inv_image R f)^-1 = inv_image (R^-1) f"
     1.8 +unfolding inv_image_def converse_def by auto
     1.9 +
    1.10  
    1.11  subsection {* Finiteness *}
    1.12