src/HOL/Relation.thy
changeset 54611 31afce809794
parent 54555 e8c5e95d338b
child 55083 0a689157e3ce
     1.1 --- a/src/HOL/Relation.thy	Thu Nov 28 22:03:41 2013 +0100
     1.2 +++ b/src/HOL/Relation.thy	Fri Nov 29 08:26:45 2013 +0100
     1.3 @@ -760,7 +760,8 @@
     1.4    by (auto simp: total_on_def)
     1.5  
     1.6  lemma finite_converse [iff]: "finite (r^-1) = finite r"  
     1.7 -  unfolding converse_def conversep_iff by (auto elim: finite_imageD simp: inj_on_def)
     1.8 +  unfolding converse_def conversep_iff using [[simproc add: finite_Collect]]
     1.9 +  by (auto elim: finite_imageD simp: inj_on_def)
    1.10  
    1.11  lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
    1.12    by (auto simp add: fun_eq_iff)