src/HOL/Hilbert_Choice.thy
changeset 27760 3aa86edac080
parent 26748 4d51ddd6aa5c
child 29655 ac31940cfb69
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Aug 06 10:43:42 2008 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Aug 06 13:57:25 2008 +0200
     1.3 @@ -307,6 +307,11 @@
     1.4  apply (rule someI2_ex, blast+)
     1.5  done
     1.6  
     1.7 +lemma wf_no_infinite_down_chainE:
     1.8 +  assumes "wf r" obtains k where "(f (Suc k), f k) \<notin> r"
     1.9 +using `wf r` wf_iff_no_infinite_down_chain[of r] by blast
    1.10 +
    1.11 +
    1.12  text{*A dynamically-scoped fact for TFL *}
    1.13  lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
    1.14    by (blast intro: someI)