# HG changeset patch # User wenzelm # Date 1375309125 -7200 # Node ID 05eb2d77b1950acda152118b83ce708da50463b5 # Parent cb53b44b958cd771a816a81fca4f78712e266f28 tuned proof; diff -r cb53b44b958c -r 05eb2d77b195 src/HOL/Library/Zorn.thy --- a/src/HOL/Library/Zorn.thy Wed Jul 31 23:41:32 2013 +0200 +++ b/src/HOL/Library/Zorn.thy Thu Aug 01 00:18:45 2013 +0200 @@ -756,8 +756,7 @@ assumes "chain\<^sub>\ R" and "\r. r \ R \ extension_on (Field r) r p" shows "extension_on (Field (\R)) (\R) p" using assms - by (simp add: chain_subset_def extension_on_def) - (metis Field_def mono_Field set_mp) + by (simp add: chain_subset_def extension_on_def) (metis mono_Field set_mp) lemma downset_on_empty [simp]: "downset_on {} p" by (auto simp: downset_on_def)