--- a/CONTRIBUTORS Sun Dec 16 22:10:37 2012 +0100
+++ b/CONTRIBUTORS Mon Dec 17 08:19:35 2012 +0100
@@ -17,6 +17,9 @@
Various improvements to Sledgehammer's Isar proof generator, including
a smart type annotation algorithm and proof shrinking.
+* December 2012: Alessandro Coglio, Kestrel
+ Contributions to HOL's Lattice library
+
* November 2012: Fabian Immler, TUM
"Symbols" dockable for Isabelle/jEdit.
--- a/src/HOL/Library/Product_Lattice.thy Sun Dec 16 22:10:37 2012 +0100
+++ b/src/HOL/Library/Product_Lattice.thy Mon Dec 17 08:19:35 2012 +0100
@@ -222,7 +222,7 @@
subsection {* Complete distributive lattices *}
-(* Contribution: Allesandro Coglio *)
+(* Contribution: Alessandro Coglio *)
instance prod ::
(complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice