src/HOL/Library/Zorn.thy
changeset 27476 964766deef47
parent 27064 267cab537760
child 28952 15a4b2cf8c34
--- a/src/HOL/Library/Zorn.thy	Thu Jul 03 18:16:40 2008 +0200
+++ b/src/HOL/Library/Zorn.thy	Thu Jul 03 19:02:33 2008 +0200
@@ -392,12 +392,13 @@
     by(simp add:wf_iff_no_infinite_down_chain) blast
 qed
 
+lemma initial_segment_of_Diff:
+  "p initial_segment_of q \<Longrightarrow> p - s initial_segment_of q - s"
+unfolding init_seg_of_def by blast
+
 lemma Chain_inits_DiffI:
   "R \<in> Chain init_seg_of \<Longrightarrow> {r - s |r. r \<in> R} \<in> Chain init_seg_of"
-apply(auto simp:Chain_def init_seg_of_def)
-apply (metis subsetD)
-apply (metis subsetD)
-done
+unfolding Chain_def by (blast intro: initial_segment_of_Diff)
 
 theorem well_ordering: "\<exists>r::('a*'a)set. Well_order r \<and> Field r = UNIV"
 proof-