| changeset 15077 | 89840837108e |
| parent 15013 | 34264f5e4691 |
| child 15085 | 5693a977a767 |
--- a/src/HOL/Real/RealDef.thy Mon Jul 26 15:48:50 2004 +0200 +++ b/src/HOL/Real/RealDef.thy Mon Jul 26 17:34:52 2004 +0200 @@ -798,6 +798,7 @@ subsubsection{*Density of the Reals*} +(*????FIXME: rename d1, d2 to x, y*) lemma real_lbound_gt_zero: "[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2" apply (rule_tac x = " (min d1 d2) /2" in exI)