summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/HOL/HOL.tex

changeset 6626 | a92d2b6e0626 |

parent 6620 | fc991461c7b9 |

child 7044 | 193a8601fabd |

--- a/doc-src/HOL/HOL.tex Mon May 10 16:48:00 1999 +0200 +++ b/doc-src/HOL/HOL.tex Mon May 10 17:02:05 1999 +0200 @@ -1784,15 +1784,16 @@ \label{sec:HOL:datatype} \index{*datatype|(} -Inductive datatypes, similar to those of \ML, frequently appear in +Inductive datatypes, similar to those of \ML, frequently appear in applications of Isabelle/HOL. In principle, such types could be defined by hand via \texttt{typedef} (see \S\ref{sec:typedef}), but this would be far too -tedious. The \ttindex{datatype} definition package of \HOL\ automates such -chores. It generates an appropriate \texttt{typedef} based on a least -fixed-point construction, and proves freeness theorems and induction rules, as -well as theorems for recursion and case combinators. The user just has to -give a simple specification of new inductive types using a notation similar to -{\ML} or Haskell. +tedious. The \ttindex{datatype} definition package of Isabelle/HOL (cf.\ +\cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores. It generates an +appropriate \texttt{typedef} based on a least fixed-point construction, and +proves freeness theorems and induction rules, as well as theorems for +recursion and case combinators. The user just has to give a simple +specification of new inductive types using a notation similar to {\ML} or +Haskell. The current datatype package can handle both mutual and indirect recursion. It also offers to represent existing types as datatypes giving the advantage