src/HOL/Conditionally_Complete_Lattices.thy

--- a/src/HOL/Conditionally_Complete_Lattices.thy	Mon May 04 16:01:36 2015 +0200
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Mon May 04 17:35:31 2015 +0200
@@ -452,6 +452,9 @@
 
 end
 
+instance complete_linorder < conditionally_complete_linorder
+  ..
+
 lemma cSup_eq_Max: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup X = Max X"
   using cSup_eq_Sup_fin[of X] Sup_fin_eq_Max[of X] by simp