Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tuned proof.
authorballarin
Tue, 03 Jun 2008 12:38:39 +0200
changeset 27064 267cab537760
parent 27063 d1d35284542f
child 27065 f68aa7b5a0f3
Tuned proof.
src/HOL/Library/Zorn.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Zorn.thy	Tue Jun 03 12:34:22 2008 +0200
+++ b/src/HOL/Library/Zorn.thy	Tue Jun 03 12:38:39 2008 +0200
@@ -305,7 +305,7 @@
   from Zorn_Lemma2[OF this]
   obtain m B where "m:Field r" "B = r^-1 `` {m}"
     "\<forall>x\<in>Field r. B \<subseteq> r^-1 `` {x} \<longrightarrow> B = r^-1 `` {x}"
-    by(auto simp:image_def) blast
+    by auto
   hence "\<forall>a\<in>Field r. (m, a) \<in> r \<longrightarrow> a = m" using po `Preorder r` `m:Field r`
     by(auto simp:subset_Image1_Image1_iff Partial_order_eq_Image1_Image1_iff)
   thus ?thesis using `m:Field r` by blast
isabelle