equal
deleted
inserted
replaced
1 (* |
1 (* |
2 Title: Orders and Lattices |
2 Title: HOL/Algebra/Lattice.thy |
3 Id: $Id$ |
3 Id: $Id$ |
4 Author: Clemens Ballarin, started 7 November 2003 |
4 Author: Clemens Ballarin, started 7 November 2003 |
5 Copyright: Clemens Ballarin |
5 Copyright: Clemens Ballarin |
6 *) |
6 *) |
7 |
7 |
8 header {* Order and Lattices *} |
8 header {* Orders and Lattices *} |
9 |
9 |
10 theory Lattice = Group: |
10 theory Lattice = Group: |
11 |
11 |
12 subsection {* Partial Orders *} |
12 subsection {* Partial Orders *} |
13 |
13 |