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;
authorwenzelm
Thu, 01 Aug 2013 00:18:45 +0200
changeset 52821 05eb2d77b195
parent 52820 cb53b44b958c
child 52822 ae938ac9a721
tuned proof;
src/HOL/Library/Zorn.thy file | annotate | diff | comparison | revisions 
--- 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>\<subseteq> R" and "\<And>r. r \<in> R \<Longrightarrow> extension_on (Field r) r p"
   shows "extension_on (Field (\<Union>R)) (\<Union>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)
isabelle