--- a/src/HOL/Hyperreal/Lim.thy Tue Sep 06 23:14:10 2005 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Tue Sep 06 23:16:48 2005 +0200
@@ -226,9 +226,9 @@
"f -- x --> L ==> f -- x --NS> L"
apply (simp add: LIM_def NSLIM_def approx_def)
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
-apply (rule_tac z = xa in eq_Abs_hypreal)
-apply (auto simp add: real_add_minus_iff starfun hypreal_minus hypreal_of_real_def hypreal_add)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, clarify)
+apply (rule_tac z = xa in eq_Abs_star)
+apply (auto simp add: real_add_minus_iff starfun hypreal_minus hypreal_of_real_def star_of_def star_n_def hypreal_add)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, clarify)
apply (drule_tac x = u in spec, clarify)
apply (drule_tac x = s in spec, clarify)
apply (subgoal_tac "\<forall>n::nat. (xa n) \<noteq> x & \<bar>(xa n) + - x\<bar> < s --> \<bar>f (xa n) + - L\<bar> < u")
@@ -270,10 +270,10 @@
apply (rule ccontr, simp)
apply (simp add: linorder_not_less)
apply (drule lemma_skolemize_LIM2, safe)
-apply (drule_tac x = "Abs_hypreal (hyprel``{X})" in spec)
-apply (auto simp add: starfun hypreal_minus hypreal_of_real_def hypreal_add)
+apply (drule_tac x = "Abs_star (starrel``{X})" in spec)
+apply (auto simp add: starfun hypreal_minus hypreal_of_real_def star_of_def star_n_def hypreal_add)
apply (drule lemma_simp [THEN real_seq_to_hypreal_Infinitesimal])
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_of_real_def hypreal_minus hypreal_add, blast)
+apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_of_real_def star_of_def star_n_def hypreal_minus hypreal_add, blast)
apply (drule spec, drule mp, assumption)
apply (drule FreeUltrafilterNat_all, ultra)
done
@@ -451,9 +451,9 @@
apply (rule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
apply (rule_tac [4] approx_minus_iff2 [THEN iffD1])
prefer 3 apply (simp add: add_commute)
-apply (rule_tac [2] z = x in eq_Abs_hypreal)
-apply (rule_tac [4] z = x in eq_Abs_hypreal)
-apply (auto simp add: starfun hypreal_of_real_def hypreal_minus hypreal_add add_assoc approx_refl hypreal_zero_def)
+apply (rule_tac [2] z = x in eq_Abs_star)
+apply (rule_tac [4] z = x in eq_Abs_star)
+apply (auto simp add: starfun hypreal_of_real_def star_of_def star_n_def hypreal_minus hypreal_add add_assoc approx_refl hypreal_zero_def)
done
lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
@@ -579,10 +579,10 @@
lemma isUCont_isNSUCont: "isUCont f ==> isNSUCont f"
apply (simp add: isNSUCont_def isUCont_def approx_def)
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe)
-apply (rule_tac z = x in eq_Abs_hypreal)
-apply (rule_tac z = y in eq_Abs_hypreal)
+apply (rule_tac z = x in eq_Abs_star)
+apply (rule_tac z = y in eq_Abs_star)
apply (auto simp add: starfun hypreal_minus hypreal_add)
-apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe)
+apply (rule bexI, rule_tac [2] lemma_starrel_refl, safe)
apply (drule_tac x = u in spec, clarify)
apply (drule_tac x = s in spec, clarify)
apply (subgoal_tac "\<forall>n::nat. abs ((xa n) + - (xb n)) < s --> abs (f (xa n) + - f (xb n)) < u")
@@ -620,8 +620,8 @@
apply (rule ccontr, simp)
apply (simp add: linorder_not_less)
apply (drule lemma_skolemize_LIM2u, safe)
-apply (drule_tac x = "Abs_hypreal (hyprel``{X})" in spec)
-apply (drule_tac x = "Abs_hypreal (hyprel``{Y})" in spec)
+apply (drule_tac x = "Abs_star (starrel``{X})" in spec)
+apply (drule_tac x = "Abs_star (starrel``{Y})" in spec)
apply (simp add: starfun hypreal_minus hypreal_add, auto)
apply (drule lemma_simpu [THEN real_seq_to_hypreal_Infinitesimal2])
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff hypreal_minus hypreal_add, blast)