author | wenzelm |

Mon May 10 17:02:05 1999 +0200 (1999-05-10) | |

changeset 6626 | a92d2b6e0626 |

parent 6625 | eca6105b1eaf |

child 6627 | c2511c9ea37e |

tuned;

doc-src/HOL/HOL.tex | file | annotate | diff | revisions | |

doc-src/HOL/logics-HOL.tex | file | annotate | diff | revisions | |

doc-src/manual.bib | file | annotate | diff | revisions |

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