src/HOL/Real/RealDef.thy
changeset 28906 5f568bfc58d7
parent 28562 4e74209f113e
     1.1 --- a/src/HOL/Real/RealDef.thy	Sat Nov 29 13:39:23 2008 +0100
     1.2 +++ b/src/HOL/Real/RealDef.thy	Sat Nov 29 13:39:45 2008 +0100
     1.3 @@ -998,7 +998,6 @@
     1.4  declare real_diff_def [symmetric, simp]
     1.5  *)
     1.6  
     1.7 -
     1.8  subsubsection{*Density of the Reals*}
     1.9  
    1.10  lemma real_lbound_gt_zero: