--- a/src/HOL/Complete_Lattices.thy Tue Mar 05 15:43:08 2013 +0100
+++ b/src/HOL/Complete_Lattices.thy Tue Mar 05 15:43:12 2013 +0100
@@ -589,6 +589,14 @@
end
+instance complete_linorder \<subseteq> complete_distrib_lattice
+ apply default
+ apply (safe intro!: INF_eqI[symmetric] sup_mono complete_lattice_class.Inf_lower
+ SUP_eqI[symmetric] inf_mono complete_lattice_class.Sup_upper)
+ apply (auto simp: not_less[symmetric]
+ Inf_less_iff less_Sup_iff le_max_iff_disj sup_max min_le_iff_disj inf_min)
+ done
+
subsection {* Complete lattice on @{typ bool} *}
instantiation bool :: complete_lattice