src/HOL/Hilbert_Choice.thy

--- a/src/HOL/Hilbert_Choice.thy	Wed Aug 06 10:43:42 2008 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Wed Aug 06 13:57:25 2008 +0200
@@ -307,6 +307,11 @@
 apply (rule someI2_ex, blast+)
 done
 
+lemma wf_no_infinite_down_chainE:
+  assumes "wf r" obtains k where "(f (Suc k), f k) \<notin> r"
+using `wf r` wf_iff_no_infinite_down_chain[of r] by blast
+
+
 text{*A dynamically-scoped fact for TFL *}
 lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
   by (blast intro: someI)