# HG changeset patch
# User nipkow
# Date 1355728775 -3600
# Node ID 765c22baa1c9b0beb1d5001ef3af152b1959c83b
# Parent  b33912e68b84618cb7d34df9abeded99742044bd
new contributor

diff -r b33912e68b84 -r 765c22baa1c9 CONTRIBUTORS
--- 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.
 
diff -r b33912e68b84 -r 765c22baa1c9 src/HOL/Library/Product_Lattice.thy
--- 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