src/HOL/Relation.thy
changeset 62343 24106dc44def
parent 62087 44841d07ef1d
child 63376 4c0cc2b356f0
     1.1 --- a/src/HOL/Relation.thy	Wed Feb 17 21:51:55 2016 +0100
     1.2 +++ b/src/HOL/Relation.thy	Wed Feb 17 21:51:56 2016 +0100
     1.3 @@ -1060,10 +1060,11 @@
     1.4  
     1.5  text\<open>Converse inclusion requires some assumptions\<close>
     1.6  lemma Image_INT_eq:
     1.7 -     "[|single_valued (r\<inverse>); A\<noteq>{}|] ==> r `` INTER A B = (\<Inter>x\<in>A. r `` B x)"
     1.8 +  "single_valued (r\<inverse>) \<Longrightarrow> A \<noteq> {} \<Longrightarrow> r `` INTER A B = (\<Inter>x\<in>A. r `` B x)"
     1.9  apply (rule equalityI)
    1.10   apply (rule Image_INT_subset) 
    1.11 -apply  (simp add: single_valued_def, blast)
    1.12 +apply (auto simp add: single_valued_def)
    1.13 +apply blast
    1.14  done
    1.15  
    1.16  lemma Image_subset_eq: "(r``A \<subseteq> B) = (A \<subseteq> - ((r^-1) `` (-B)))"