--- a/src/HOL/Algebra/Lattice.thy Thu Aug 03 14:53:57 2006 +0200
+++ b/src/HOL/Algebra/Lattice.thy Thu Aug 03 14:57:26 2006 +0200
@@ -5,15 +5,17 @@
Copyright: Clemens Ballarin
*)
-header {* Orders and Lattices *}
+theory Lattice imports Main begin
-theory Lattice imports Main begin
+
+section {* Orders and Lattices *}
text {* Object with a carrier set. *}
record 'a partial_object =
carrier :: "'a set"
+
subsection {* Partial Orders *}
record 'a order = "'a partial_object" +
@@ -822,9 +824,10 @@
(* TODO: prove dual version *)
+
subsection {* Examples *}
-subsubsection {* Powerset of a set is a complete lattice *}
+subsubsection {* Powerset of a Set is a Complete Lattice *}
theorem powerset_is_complete_lattice:
"complete_lattice (| carrier = Pow A, le = op \<subseteq> |)"