# HG changeset patch
# User huffman
# Date 1215104553 -7200
# Node ID 964766deef4731eddb33d7d311a2424a5ae23402
# Parent  61b979a2c8209cd7a1f43d96280960b3f3394bea
fixed extremely slow proof of Chain_inits_DiffI

diff -r 61b979a2c820 -r 964766deef47 src/HOL/Library/Zorn.thy
--- 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-