src/HOL/Conditionally_Complete_Lattices.thy
changeset 53216 ad2e09c30aa8
parent 53215 5e47c31c6f7c
child 54257 5c7a3b6b05a9
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue Aug 27 14:37:56 2013 +0200
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Aug 27 16:06:27 2013 +0200
     1.3 @@ -246,7 +246,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -class linear_continuum = conditionally_complete_linorder + inner_dense_linorder +
     1.8 +class linear_continuum = conditionally_complete_linorder + dense_linorder +
     1.9    assumes UNIV_not_singleton: "\<exists>a b::'a. a \<noteq> b"
    1.10  begin
    1.11