# HG changeset patch
# User hoelzl
# Date 1362494592 -3600
# Node ID 8c10293e7ea71c71f117e8ec6a7023db4e12a55d
# Parent  5e6296afe08d6804a3dbdb929f0174569f61795e
complete_linorder is also a complete_distrib_lattice

diff -r 5e6296afe08d -r 8c10293e7ea7 src/HOL/Complete_Lattices.thy
--- 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