src/HOL/Algebra/Lattice.thy
changeset 14577 dbb95b825244
parent 14551 2cb6ff394bfb
child 14651 02b8f3bcf7fe
     1.1 --- a/src/HOL/Algebra/Lattice.thy	Fri Apr 16 04:06:52 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Lattice.thy	Fri Apr 16 04:07:10 2004 +0200
     1.3 @@ -5,9 +5,9 @@
     1.4    Copyright: Clemens Ballarin
     1.5  *)
     1.6  
     1.7 -theory Lattice = Group:
     1.8 +header {* Order and Lattices *}
     1.9  
    1.10 -section {* Order and Lattices *}
    1.11 +theory Lattice = Group:
    1.12  
    1.13  subsection {* Partial Orders *}
    1.14