# HG changeset patch
# User huffman
# Date 1179862324 -7200
# Node ID e5670ceef56f56f515b7d393d34507468ee46073
# Parent  be166bf115d4a4b14d8ce50b5305a30f377dfca2
new simp rule Infinitesimal_of_hypreal_iff

diff -r be166bf115d4 -r e5670ceef56f src/HOL/Hyperreal/HLim.thy
--- a/src/HOL/Hyperreal/HLim.thy	Tue May 22 19:58:54 2007 +0200
+++ b/src/HOL/Hyperreal/HLim.thy	Tue May 22 21:32:04 2007 +0200
@@ -106,7 +106,6 @@
 apply (simp add: NSLIM_def)
 apply (rule_tac x="star_of a + of_hypreal epsilon" in exI)
 apply (simp add: hypreal_epsilon_not_zero approx_def)
-apply (rule Infinitesimal_hnorm_iff [THEN iffD1], simp)
 done
 
 lemma NSLIM_not_zero:
diff -r be166bf115d4 -r e5670ceef56f src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Tue May 22 19:58:54 2007 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Tue May 22 21:32:04 2007 +0200
@@ -362,6 +362,15 @@
   "(hnorm x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
 by (simp add: Infinitesimal_def)
 
+lemma Infinitesimal_hrabs_iff [iff]:
+  "(abs (x::hypreal) \<in> Infinitesimal) = (x \<in> Infinitesimal)"
+by (simp add: abs_if)
+
+lemma Infinitesimal_of_hypreal_iff [simp]:
+  "((of_hypreal x::'a::real_normed_algebra_1 star) \<in> Infinitesimal) =
+   (x \<in> Infinitesimal)"
+by (subst Infinitesimal_hnorm_iff [symmetric], simp)
+
 lemma Infinitesimal_diff:
      "[| x \<in> Infinitesimal;  y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
 by (simp add: diff_def Infinitesimal_add)
@@ -506,10 +515,6 @@
 lemma not_Infinitesimal_not_zero2: "x \<in> HFinite - Infinitesimal ==> x \<noteq> 0"
 by auto
 
-lemma Infinitesimal_hrabs_iff [iff]:
-     "(abs (x::hypreal) \<in> Infinitesimal) = (x \<in> Infinitesimal)"
-by (auto simp add: abs_if)
-
 lemma HFinite_diff_Infinitesimal_hrabs:
   "(x::hypreal) \<in> HFinite - Infinitesimal ==> abs x \<in> HFinite - Infinitesimal"
 by blast