src/HOL/Conditionally_Complete_Lattices.thy
changeset 60172 423273355b55
parent 59452 2538b2c51769
child 60615 e5fa1d5d3952
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Mon May 04 16:01:36 2015 +0200
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Mon May 04 17:35:31 2015 +0200
     1.3 @@ -452,6 +452,9 @@
     1.4  
     1.5  end
     1.6  
     1.7 +instance complete_linorder < conditionally_complete_linorder
     1.8 +  ..
     1.9 +
    1.10  lemma cSup_eq_Max: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X"
    1.11    using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp
    1.12