diff -r f51d4a302962 -r 5386df44a037 doc-src/TutorialI/document/inductive0.tex --- a/doc-src/TutorialI/document/inductive0.tex Tue Aug 28 18:46:15 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,31 +0,0 @@ -\chapter{Inductively Defined Sets} \label{chap:inductive} -\index{inductive definitions|(} - -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. 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. - -\begin{warn} -Predicates can also be defined inductively. -See {\S}\ref{sec:ind-predicates}. -\end{warn} - -\input{Even} -\input{Mutual} -\input{Star} - -\section{Advanced Inductive Definitions} -\label{sec:adv-ind-def} -\input{Advanced} - -\input{AB} - -\index{inductive definitions|)}