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

author | paulson |

Wed, 25 Oct 2000 17:44:59 +0200 | |

changeset 10327 | 19214ac381cf |

parent 10326 | d4fe5ce8a5d5 |

child 10328 | bf33cbd76c05 |

inputs Even.tex

--- a/doc-src/TutorialI/Inductive/inductive.tex Wed Oct 25 17:44:48 2000 +0200 +++ b/doc-src/TutorialI/Inductive/inductive.tex Wed Oct 25 17:44:59 2000 +0200 @@ -5,13 +5,15 @@ This chapter is dedicated to the most important definition principle after recursive functions and datatypes: inductively defined sets. -We start with a simple example \ldots . A slightly more complicated example, the +We start with a simple example: the set of even numbers. +A slightly more complicated example, the reflexive transitive closure, is the subject of {\S}\ref{sec:rtc}. In particular, some standard induction heuristics are discussed. To demonstrate the versatility of inductive definitions, {\S}\ref{sec:CFG} presents a case study from the realm of context-free grammars. The chapter closes with a discussion of advanced forms of inductive definitions. +\input{Inductive/Even} \input{Inductive/document/Star} \input{Inductive/document/AB}