--- 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
--- a/doc-src/HOL/logics-HOL.tex Mon May 10 16:48:00 1999 +0200
+++ b/doc-src/HOL/logics-HOL.tex Mon May 10 17:02:05 1999 +0200
@@ -19,9 +19,9 @@
\author{Tobias Nipkow\footnote
{Institut f\"ur Informatik, Technische Universit\"at M\"unchen,
- \texttt{nipkow@in.tum.de}},
+ \texttt{nipkow@in.tum.de}} and
Lawrence C. Paulson\footnote
-{Computer Laboratory, University of Cambridge, \texttt{lcp@cl.cam.ac.uk}},
+{Computer Laboratory, University of Cambridge, \texttt{lcp@cl.cam.ac.uk}} and
Markus Wenzel\footnote
{Institut f\"ur Informatik, Technische Universit\"at M\"unchen,
\texttt{wenzelm@in.tum.de}}}
--- a/doc-src/manual.bib Mon May 10 16:48:00 1999 +0200
+++ b/doc-src/manual.bib Mon May 10 17:02:05 1999 +0200
@@ -91,12 +91,11 @@
@InProceedings{Berghofer-Wenzel:1999:TPHOL,
author = {Stefan Berghofer and Markus Wenzel},
- title = {Inductive datatypes in HOL --- lessons learned in Formal-Logic Engineering},
+ title = {Inductive datatypes in {HOL} --- lessons learned in {F}ormal-{L}ogic {E}ngineering},
booktitle = {Theorem Proving in Higher Order Logics (TPHOLs'99)},
series = LNCS,
year = 1999,
- publisher = Springer,
- note = {to appear}
+ publisher = Springer
}
@book{Bird-Wadler,author="Richard Bird and Philip Wadler",