# HG changeset patch
# User huffman
# Date 1159399950 -7200
# Node ID f45aca87b64ef06a9bfa1c78db863e060a5b559b
# Parent  09cf0e407a455f7d1a1e7be07b7830f2379330e7
add lemma hypreal_epsilon_gt_zero

diff -r 09cf0e407a45 -r f45aca87b64e src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Thu Sep 28 01:26:28 2006 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Sep 28 01:32:30 2006 +0200
@@ -368,4 +368,7 @@
 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
 by (simp add: epsilon_def omega_def star_n_inverse)
 
+lemma hypreal_epsilon_gt_zero: "0 < epsilon"
+by (simp add: hypreal_epsilon_inverse_omega)
+
 end