tuned;
authorwenzelm
Mon May 10 17:02:05 1999 +0200 (1999-05-10)
changeset 6626a92d2b6e0626
parent 6625 eca6105b1eaf
child 6627 c2511c9ea37e
tuned;
doc-src/HOL/HOL.tex
doc-src/HOL/logics-HOL.tex
doc-src/manual.bib
     1.1 --- a/doc-src/HOL/HOL.tex	Mon May 10 16:48:00 1999 +0200
     1.2 +++ b/doc-src/HOL/HOL.tex	Mon May 10 17:02:05 1999 +0200
     1.3 @@ -1784,15 +1784,16 @@
     1.4  \label{sec:HOL:datatype}
     1.5  \index{*datatype|(}
     1.6  
     1.7 -Inductive datatypes, similar to those of \ML, frequently appear in 
     1.8 +Inductive datatypes, similar to those of \ML, frequently appear in
     1.9  applications of Isabelle/HOL.  In principle, such types could be defined by
    1.10  hand via \texttt{typedef} (see \S\ref{sec:typedef}), but this would be far too
    1.11 -tedious.  The \ttindex{datatype} definition package of \HOL\ automates such
    1.12 -chores.  It generates an appropriate \texttt{typedef} based on a least
    1.13 -fixed-point construction, and proves freeness theorems and induction rules, as
    1.14 -well as theorems for recursion and case combinators.  The user just has to
    1.15 -give a simple specification of new inductive types using a notation similar to
    1.16 -{\ML} or Haskell.
    1.17 +tedious.  The \ttindex{datatype} definition package of Isabelle/HOL (cf.\ 
    1.18 +\cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores.  It generates an
    1.19 +appropriate \texttt{typedef} based on a least fixed-point construction, and
    1.20 +proves freeness theorems and induction rules, as well as theorems for
    1.21 +recursion and case combinators.  The user just has to give a simple
    1.22 +specification of new inductive types using a notation similar to {\ML} or
    1.23 +Haskell.
    1.24  
    1.25  The current datatype package can handle both mutual and indirect recursion.
    1.26  It also offers to represent existing types as datatypes giving the advantage
     2.1 --- a/doc-src/HOL/logics-HOL.tex	Mon May 10 16:48:00 1999 +0200
     2.2 +++ b/doc-src/HOL/logics-HOL.tex	Mon May 10 17:02:05 1999 +0200
     2.3 @@ -19,9 +19,9 @@
     2.4  
     2.5  \author{Tobias Nipkow\footnote
     2.6  {Institut f\"ur Informatik, Technische Universit\"at M\"unchen,
     2.7 - \texttt{nipkow@in.tum.de}},
     2.8 + \texttt{nipkow@in.tum.de}} and
     2.9  Lawrence C. Paulson\footnote
    2.10 -{Computer Laboratory, University of Cambridge, \texttt{lcp@cl.cam.ac.uk}},
    2.11 +{Computer Laboratory, University of Cambridge, \texttt{lcp@cl.cam.ac.uk}} and
    2.12  Markus Wenzel\footnote
    2.13  {Institut f\"ur Informatik, Technische Universit\"at M\"unchen,
    2.14   \texttt{wenzelm@in.tum.de}}}
     3.1 --- a/doc-src/manual.bib	Mon May 10 16:48:00 1999 +0200
     3.2 +++ b/doc-src/manual.bib	Mon May 10 17:02:05 1999 +0200
     3.3 @@ -91,12 +91,11 @@
     3.4  
     3.5  @InProceedings{Berghofer-Wenzel:1999:TPHOL,
     3.6    author = 	 {Stefan Berghofer and Markus Wenzel},
     3.7 -  title = 	 {Inductive datatypes in HOL --- lessons learned in Formal-Logic Engineering},
     3.8 +  title = 	 {Inductive datatypes in {HOL} --- lessons learned in {F}ormal-{L}ogic {E}ngineering},
     3.9    booktitle = 	 {Theorem Proving in Higher Order Logics (TPHOLs'99)},
    3.10    series =	 LNCS,
    3.11    year =	 1999,
    3.12 -  publisher =	 Springer,
    3.13 -  note =	 {to appear}
    3.14 +  publisher =	 Springer
    3.15  }
    3.16  
    3.17  @book{Bird-Wadler,author="Richard Bird and Philip Wadler",