src/HOL/NSA/NSA.thy

  -------------------------------------*)
 lemma FreeUltrafilterNat_const_Finite:
      "eventually (\<lambda>n. norm (X n) = u) FreeUltrafilterNat ==> star_n X \<in> HFinite"
 apply (rule FreeUltrafilterNat_HFinite)
 apply (rule_tac x = "u + 1" in exI)
-apply (auto elim: eventually_elim1)
+apply (auto elim: eventually_mono)
 done
 
 lemma HInfinite_FreeUltrafilterNat:
      "star_n X \<in> HInfinite ==> \<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat"
 apply (drule HInfinite_HFinite_iff [THEN iffD1])
 apply (simp add: HFinite_FreeUltrafilterNat_iff)
 apply (rule allI, drule_tac x="u + 1" in spec)
 apply (simp add: FreeUltrafilterNat.eventually_not_iff[symmetric])
-apply (auto elim: eventually_elim1)
+apply (auto elim: eventually_mono)
 done
 
 lemma lemma_Int_HI:
      "{n. norm (Xa n) < u} Int {n. X n = Xa n} \<subseteq> {n. norm (X n) < (u::real)}"
 by auto

 
 theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
 apply (simp add: omega_def)
 apply (rule FreeUltrafilterNat_HInfinite)
 apply clarify
-apply (rule_tac u1 = "u-1" in eventually_mono' [OF FreeUltrafilterNat_nat_gt_real])
+apply (rule_tac u1 = "u-1" in eventually_mono [OF FreeUltrafilterNat_nat_gt_real])
 apply auto
 done
 
 (*-----------------------------------------------
        Epsilon is a member of Infinitesimal

 lemma real_seq_to_hypreal_Infinitesimal:
      "\<forall>n. norm(X n - x) < inverse(real(Suc n))
      ==> star_n X - star_of x \<in> Infinitesimal"
 unfolding star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse
 by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
-         intro: order_less_trans elim!: eventually_elim1)
+         intro: order_less_trans elim!: eventually_mono)
 
 lemma real_seq_to_hypreal_approx:
      "\<forall>n. norm(X n - x) < inverse(real(Suc n))
       ==> star_n X @= star_of x"
 by (metis bex_Infinitesimal_iff real_seq_to_hypreal_Infinitesimal)

 lemma real_seq_to_hypreal_Infinitesimal2:
      "\<forall>n. norm(X n - Y n) < inverse(real(Suc n))
       ==> star_n X - star_n Y \<in> Infinitesimal"
 unfolding Infinitesimal_FreeUltrafilterNat_iff star_n_diff
 by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
-         intro: order_less_trans elim!: eventually_elim1)
+         intro: order_less_trans elim!: eventually_mono)
 
 end