src/HOL/Real_Vector_Spaces.thy
changeset 51775 408d937c9486
parent 51774 916271d52466
child 52381 63eec9cea2c7
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu Apr 25 10:35:56 2013 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu Apr 25 11:59:21 2013 +0200
     1.3 @@ -860,7 +860,7 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -instance real :: connected_linorder_topology ..
     1.8 +instance real :: linear_continuum_topology ..
     1.9  
    1.10  lemmas open_real_greaterThan = open_greaterThan[where 'a=real]
    1.11  lemmas open_real_lessThan = open_lessThan[where 'a=real]