# HG changeset patch
# User wenzelm
# Date 926348525 -7200
# Node ID a92d2b6e06262ddb2e3922b088e19706d7b9a496
# Parent  eca6105b1eaf14ebfc777fdc0ecf962fba4fe21c
tuned;

diff -r eca6105b1eaf -r a92d2b6e0626 doc-src/HOL/HOL.tex
--- 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
diff -r eca6105b1eaf -r a92d2b6e0626 doc-src/HOL/logics-HOL.tex
--- 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}}}
diff -r eca6105b1eaf -r a92d2b6e0626 doc-src/manual.bib
--- 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",