| changeset 14577 | dbb95b825244 |
| parent 14551 | 2cb6ff394bfb |
| child 14651 | 02b8f3bcf7fe |
--- a/src/HOL/Algebra/Lattice.thy Fri Apr 16 04:06:52 2004 +0200 +++ b/src/HOL/Algebra/Lattice.thy Fri Apr 16 04:07:10 2004 +0200 @@ -5,9 +5,9 @@ Copyright: Clemens Ballarin *) -theory Lattice = Group: +header {* Order and Lattices *} -section {* Order and Lattices *} +theory Lattice = Group: subsection {* Partial Orders *}