doc-src/TutorialI/Misc/pairs.thy
changeset 10795 9e888d60d3e5
parent 10543 8e4307d1207a
child 10839 1f93f5a27de6
equal deleted inserted replaced
10794:65d18005d802 10795:9e888d60d3e5
    20 as a degenerate product with 0 components.
    20 as a degenerate product with 0 components.
    21 \item
    21 \item
    22 Products, like type @{typ nat}, are datatypes, which means
    22 Products, like type @{typ nat}, are datatypes, which means
    23 in particular that @{text induct_tac} and @{text case_tac} are applicable to
    23 in particular that @{text induct_tac} and @{text case_tac} are applicable to
    24 terms of product type.
    24 terms of product type.
       
    25 Both replace the term by tuple of variables.
    25 \item
    26 \item
    26 Instead of tuples with many components (where ``many'' is not much above 2),
    27 Tuples with more than two or three components become unwieldy;
    27 it is preferable to use records.
    28 records are preferable.
    28 \end{itemize}
    29 \end{itemize}
    29 For more information on pairs and records see Chapter~\ref{ch:more-types}.
    30 For more information on pairs and records see Chapter~\ref{ch:more-types}.
    30 *}
    31 *}
    31 (*<*)
    32 (*<*)
    32 end
    33 end