--- a/src/HOL/Real/RealDef.thy Sat Nov 29 13:39:23 2008 +0100
+++ b/src/HOL/Real/RealDef.thy Sat Nov 29 13:39:45 2008 +0100
@@ -998,7 +998,6 @@
declare real_diff_def [symmetric, simp]
*)
-
subsubsection{*Density of the Reals*}
lemma real_lbound_gt_zero: