src/HOL/Real.thy

--- a/src/HOL/Real.thy	Thu Apr 25 10:31:10 2013 +0200
+++ b/src/HOL/Real.thy	Wed Apr 24 13:28:30 2013 +0200
@@ -10,7 +10,7 @@
 header {* Development of the Reals using Cauchy Sequences *}
 
 theory Real
-imports Rat Conditional_Complete_Lattices
+imports Rat Conditionally_Complete_Lattices
 begin
 
 text {*
@@ -925,7 +925,7 @@
 qed
 
 
-instantiation real :: conditional_complete_linorder
+instantiation real :: conditionally_complete_linorder
 begin
 
 subsection{*Supremum of a set of reals*}