# HG changeset patch
# User huffman
# Date 1159394026 -7200
# Node ID f7f2d03fe6f9a1ed33f729562828a14cbc880921
# Parent  4bcf492c6c9dbb53648074eb5da165615b1f353f
add lemmas InfinitesimalI2, InfinitesimalD2

diff -r 4bcf492c6c9d -r f7f2d03fe6f9 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Wed Sep 27 23:41:12 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Wed Sep 27 23:53:46 2006 +0200
@@ -345,6 +345,14 @@
       "x \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> hnorm x < r"
 by (simp add: Infinitesimal_def)
 
+lemma InfinitesimalI2:
+  "(\<And>r. 0 < r \<Longrightarrow> hnorm x < star_of r) \<Longrightarrow> x \<in> Infinitesimal"
+by (auto simp add: Infinitesimal_def SReal_def)
+
+lemma InfinitesimalD2:
+  "\<lbrakk>x \<in> Infinitesimal; 0 < r\<rbrakk> \<Longrightarrow> hnorm x < star_of r"
+by (auto simp add: Infinitesimal_def SReal_def)
+
 lemma Infinitesimal_zero [iff]: "0 \<in> Infinitesimal"
 by (simp add: Infinitesimal_def)