# HG changeset patch # User wenzelm # Date 1214227611 -7200 # Node ID 464ac1c815ec498eff85ff1b84e0f923390f3684 # Parent b7443e5a5335f4d3f586aa45e5c823a63d72da53 induct_tac/case_tac: nested tuples are split as expected; 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.