src/HOL/Real.thy
changeset 51775 408d937c9486
parent 51773 9328c6681f3c
child 51956 a4d81cdebf8b
     1.1 --- a/src/HOL/Real.thy	Thu Apr 25 10:35:56 2013 +0200
     1.2 +++ b/src/HOL/Real.thy	Thu Apr 25 11:59:21 2013 +0200
     1.3 @@ -925,7 +925,7 @@
     1.4  qed
     1.5  
     1.6  
     1.7 -instantiation real :: conditionally_complete_linorder
     1.8 +instantiation real :: linear_continuum
     1.9  begin
    1.10  
    1.11  subsection{*Supremum of a set of reals*}
    1.12 @@ -970,6 +970,9 @@
    1.13        using x z by (force intro: Sup_least)
    1.14      then show "z \<le> Inf X" 
    1.15          by (auto simp add: Inf_real_def) }
    1.16 +
    1.17 +  show "\<exists>a b::real. a \<noteq> b"
    1.18 +    using zero_neq_one by blast
    1.19  qed
    1.20  end
    1.21