src/HOL/Real.thy

--- a/src/HOL/Real.thy	Wed Jun 15 15:55:02 2016 +0200
+++ b/src/HOL/Real.thy	Fri Jun 17 09:44:16 2016 +0200
@@ -10,7 +10,7 @@
 section \<open>Development of the Reals using Cauchy Sequences\<close>
 
 theory Real
-imports Rat Conditionally_Complete_Lattices
+imports Rat
 begin
 
 text \<open>
@@ -961,7 +961,6 @@
 qed
 end
 
-
 subsection \<open>Hiding implementation details\<close>
 
 hide_const (open) vanishes cauchy positive Real