src/HOL/Relation.thy
changeset 44921 58eef4843641
parent 44278 1220ecb81e8f
child 45012 060f76635bfe
     1.1 --- a/src/HOL/Relation.thy	Tue Sep 13 08:21:51 2011 -0700
     1.2 +++ b/src/HOL/Relation.thy	Tue Sep 13 17:07:33 2011 -0700
     1.3 @@ -420,7 +420,7 @@
     1.4  by blast
     1.5  
     1.6  lemma fst_eq_Domain: "fst ` R = Domain R"
     1.7 -by (auto intro!:image_eqI)
     1.8 +  by force
     1.9  
    1.10  lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
    1.11  by auto
    1.12 @@ -471,7 +471,7 @@
    1.13  by blast
    1.14  
    1.15  lemma snd_eq_Range: "snd ` R = Range R"
    1.16 -by (auto intro!:image_eqI)
    1.17 +  by force
    1.18  
    1.19  
    1.20  subsection {* Field *}