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

author | wenzelm |

Mon, 10 May 1999 17:02:05 +0200 | |

changeset 6626 | a92d2b6e0626 |

parent 6625 | eca6105b1eaf |

child 6627 | c2511c9ea37e |

tuned;

--- 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",