src/HOL/Real.thy
changeset 51773 9328c6681f3c
parent 51539 625d2ec0bbff
child 51775 408d937c9486
     1.1 --- a/src/HOL/Real.thy	Thu Apr 25 10:31:10 2013 +0200
     1.2 +++ b/src/HOL/Real.thy	Wed Apr 24 13:28:30 2013 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  header {* Development of the Reals using Cauchy Sequences *}
     1.5  
     1.6  theory Real
     1.7 -imports Rat Conditional_Complete_Lattices
     1.8 +imports Rat Conditionally_Complete_Lattices
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -925,7 +925,7 @@
    1.13  qed
    1.14  
    1.15  
    1.16 -instantiation real :: conditional_complete_linorder
    1.17 +instantiation real :: conditionally_complete_linorder
    1.18  begin
    1.19  
    1.20  subsection{*Supremum of a set of reals*}