1.1 --- a/src/HOL/Limits.thy	Mon Mar 12 17:27:52 2012 +0100
     1.2 +++ b/src/HOL/Limits.thy	Mon Mar 12 21:28:10 2012 +0100
     1.3 @@ -111,6 +111,26 @@
     1.4    then show ?thesis by (auto elim: eventually_elim2)
     1.5  qed
     1.6  
     1.7 +ML {*
     1.8 +  fun ev_elim_tac ctxt thms thm = let
     1.9 +      val thy = Proof_Context.theory_of ctxt
    1.10 +      val mp_thms = thms RL [@{thm eventually_rev_mp}]
    1.11 +      val raw_elim_thm =
    1.12 +        (@{thm allI} RS @{thm always_eventually})
    1.13 +        |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
    1.14 +        |> fold (fn _ => fn thm => @{thm impI} RS thm) thms
    1.15 +      val cases_prop = prop_of (raw_elim_thm RS thm)
    1.16 +      val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
    1.17 +    in
    1.18 +      CASES cases (rtac raw_elim_thm 1) thm
    1.19 +    end
    1.20 +
    1.21 +  fun eventually_elim_setup name =
    1.22 +    Method.setup name (Scan.succeed (fn ctxt => METHOD_CASES (ev_elim_tac ctxt)))
    1.23 +      "elimination of eventually quantifiers"
    1.24 +*}
    1.25 +
    1.26 +setup {* eventually_elim_setup @{binding "eventually_elim"} *}
    1.27  
    1.28  
    1.29  subsection {* Finer-than relation *}