Tuned proof.
authorballarin
Tue Jun 03 12:38:39 2008 +0200 (2008-06-03)
changeset 27064267cab537760
parent 27063 d1d35284542f
child 27065 f68aa7b5a0f3
Tuned proof.
src/HOL/Library/Zorn.thy
     1.1 --- a/src/HOL/Library/Zorn.thy	Tue Jun 03 12:34:22 2008 +0200
     1.2 +++ b/src/HOL/Library/Zorn.thy	Tue Jun 03 12:38:39 2008 +0200
     1.3 @@ -305,7 +305,7 @@
     1.4    from Zorn_Lemma2[OF this]
     1.5    obtain m B where "m:Field r" "B = r^-1 `` {m}"
     1.6      "\<forall>x\<in>Field r. B \<subseteq> r^-1 `` {x} \<longrightarrow> B = r^-1 `` {x}"
     1.7 -    by(auto simp:image_def) blast
     1.8 +    by auto
     1.9    hence "\<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m" using po `Preorder r` `m:Field r`
    1.10      by(auto simp:subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff)
    1.11    thus ?thesis using `m:Field r` by blast