--- a/src/HOL/ex/Tuple.thy	Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/Tuple.thy	Wed Sep 14 22:08:08 2005 +0200
@@ -1,11 +1,6 @@
 (*  Title:      HOL/ex/Tuple.thy
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
-
-Properly nested products (see also theory Prod).
-
-Unquestionably, this should be used as the standard representation of
-tuples in HOL, but it breaks many existing theories!
 *)
 
 header {* Properly nested products *}