diff -r 449e1a1bb7a8 -r d848c6693185 doc-src/TutorialI/Inductive/inductive.tex --- a/doc-src/TutorialI/Inductive/inductive.tex Fri Feb 16 00:36:21 2001 +0100 +++ b/doc-src/TutorialI/Inductive/inductive.tex Fri Feb 16 06:46:20 2001 +0100 @@ -5,19 +5,21 @@ This chapter is dedicated to the most important definition principle after recursive functions and datatypes: inductively defined sets. -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. +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. Advanced forms of inductive definitions are discussed in +{\S}\ref{sec:adv-ind-def}. To demonstrate the versatility of inductive +definitions, the chapter closes with a case study from the realm of +context-free grammars. The first two sections are required reading for anybody +interested in mathematical modelling. \input{Inductive/even-example} \input{Inductive/document/Mutual} \input{Inductive/document/Star} \section{Advanced inductive definitions} +\label{sec:adv-ind-def} \input{Inductive/advanced-examples} \input{Inductive/document/AB}