--- a/src/HOL/Set.thy Fri Mar 16 21:32:10 2007 +0100
+++ b/src/HOL/Set.thy Fri Mar 16 21:32:11 2007 +0100
@@ -1036,12 +1036,15 @@
and [symmetric, defn] = atomize_ball
-subsection {* Further set-theory lemmas *}
+subsection {* Order on sets *}
instance set :: (type) order
by (intro_classes,
(assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+)
+
+subsection {* Further set-theory lemmas *}
+
subsubsection {* Derived rules involving subsets. *}
text {* @{text insert}. *}
@@ -2116,6 +2119,14 @@
order_trans_rules set_rev_mp set_mp
+subsection {* Sets as lattice *}
+
+instance set :: (type) distrib_lattice
+ inf_set_eq: "inf A B \<equiv> A \<inter> B"
+ sup_set_eq: "sup A B \<equiv> A \<union> B"
+ by intro_classes (auto simp add: inf_set_eq sup_set_eq)
+
+
subsection {* Basic ML bindings *}
ML {*