# HG changeset patch # User haftmann # Date 1312870042 -7200 # Node ID 50c067b51135415777ab6818d83ab9356c367d62 # Parent cedaca00789f62fc74cced4eebd66f75df77bc44 tuned header diff -r cedaca00789f -r 50c067b51135 src/HOL/Complete_Lattice.thy --- a/src/HOL/Complete_Lattice.thy Tue Aug 09 08:06:15 2011 +0200 +++ b/src/HOL/Complete_Lattice.thy Tue Aug 09 08:07:22 2011 +0200 @@ -1,6 +1,6 @@ (* Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel; Florian Haftmann, TU Muenchen *) -header {* Complete lattices, with special focus on sets *} +header {* Complete lattices *} theory Complete_Lattice imports Set