author | huffman |
Thu, 28 Sep 2006 01:32:30 +0200 | |
changeset 20753 | f45aca87b64e |
parent 20752 | 09cf0e407a45 |
child 20754 | 9c053a494dc6 |
--- 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