diff -r 59c1bfc81d91 -r 3a4d03d1a31b src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Wed Aug 31 15:46:36 2005 +0200
+++ b/src/HOL/Library/Product_ord.thy	Wed Aug 31 15:46:37 2005 +0200
@@ -3,7 +3,7 @@
     Author:     Norbert Voelker
 *)
 
-header {* Instantiation of order classes for product types *}
+header {* Order on product types *}
 
 theory Product_ord
 imports Main