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