diff -r b7443e5a5335 -r 464ac1c815ec doc-src/TutorialI/Misc/pairs.thy --- a/doc-src/TutorialI/Misc/pairs.thy Mon Jun 23 15:26:49 2008 +0200 +++ b/doc-src/TutorialI/Misc/pairs.thy Mon Jun 23 15:26:51 2008 +0200 @@ -22,7 +22,8 @@ Products, like type @{typ nat}, are datatypes, which means in particular that @{text induct_tac} and @{text case_tac} are applicable to terms of product type. -Both replace the term by a pair of variables. +Both split the term into a number of variables corresponding to the tuple structure +(up to 7 components). \item Tuples with more than two or three components become unwieldy; records are preferable.