summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 29 Nov 2000 17:23:27 +0100 | |

changeset 10539 | 5929460a41df |

parent 10538 | d1bf9ca9008d |

child 10540 | abe2322fa422 |

*** empty log message ***

--- a/doc-src/TutorialI/Misc/document/pairs.tex Wed Nov 29 13:44:26 2000 +0100 +++ b/doc-src/TutorialI/Misc/document/pairs.tex Wed Nov 29 17:23:27 2000 +0100 @@ -15,16 +15,21 @@ $\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}. +Remarks: +\begin{itemize} +\item There is also the type \isaindexbold{unit}, which contains exactly one element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed -as a degenerate Cartesian product of 0 types. - -Note that products, like type \isa{nat}, are datatypes, which means +as a degenerate product with 0 components. +\item +Products, like type \isa{nat}, are datatypes, which means in particular that \isa{induct{\isacharunderscore}tac} and \isa{case{\isacharunderscore}tac} are applicable to -products (see \S\ref{sec:products}). - +terms of product type. +\item Instead of tuples with many components (where ``many'' is not much above 2), -it is far preferable to use records (see \S\ref{sec:records}).% +it is preferable to use records. +\end{itemize} +For more information on pairs and records see Chapter~\ref{ch:more-types}.% \end{isamarkuptext}% \end{isabellebody}% %%% Local Variables:

--- a/doc-src/TutorialI/Misc/pairs.thy Wed Nov 29 13:44:26 2000 +0100 +++ b/doc-src/TutorialI/Misc/pairs.thy Wed Nov 29 17:23:27 2000 +0100 @@ -13,16 +13,21 @@ $\tau@1 \times (\tau@2 \times \tau@3)$. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}. +Remarks: +\begin{itemize} +\item There is also the type \isaindexbold{unit}, which contains exactly one element denoted by \ttindexboldpos{()}{$Isatype}. This type can be viewed -as a degenerate Cartesian product of 0 types. - -Note that products, like type @{typ nat}, are datatypes, which means +as a degenerate product with 0 components. +\item +Products, like type @{typ nat}, are datatypes, which means in particular that @{text induct_tac} and @{text case_tac} are applicable to -products (see \S\ref{sec:products}). - +terms of product type. +\item Instead of tuples with many components (where ``many'' is not much above 2), -it is far preferable to use records (see \S\ref{sec:records}). +it is preferable to use records. +\end{itemize} +For more information on pairs and records see Chapter~\ref{ch:more-types}. *} (*<*) end

--- a/doc-src/TutorialI/Types/types.tex Wed Nov 29 13:44:26 2000 +0100 +++ b/doc-src/TutorialI/Types/types.tex Wed Nov 29 17:23:27 2000 +0100 @@ -1,4 +1,5 @@ \chapter{More about Types} +\label{ch:more-types} So far we have learned about a few basic types (for example \isa{bool} and \isa{nat}), type abbreviations (\isacommand{types}) and recursive datatpes @@ -18,7 +19,9 @@ \section{Numbers} \label{sec:numbers} +\index{product type|(} \input{Types/document/Pairs} +\index{product type|)} % Check refs to this section to see what is expected of it. % Mention type unit