src/HOL/Real_Vector_Spaces.thy
changeset 51774 916271d52466
parent 51642 400ec5ae7f8f
child 51775 408d937c9486
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Apr 24 13:28:30 2013 +0200
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu Apr 25 10:35:56 2013 +0200
     1.3 @@ -860,7 +860,7 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -instance real :: linear_continuum_topology ..
     1.8 +instance real :: connected_linorder_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]