doc-src/TutorialI/fp.tex
changeset 10181 c07860c826c5
parent 9933 9feb1e0c4cb3
child 10237 875bf54b5d74
equal deleted inserted replaced
10180:149878bae19c 10181:c07860c826c5
   557 \subsection{Proving termination}
   557 \subsection{Proving termination}
   558 
   558 
   559 \input{Recdef/document/termination.tex}
   559 \input{Recdef/document/termination.tex}
   560 
   560 
   561 \subsection{Simplification with recdef}
   561 \subsection{Simplification with recdef}
       
   562 \label{sec:recdef-simplification}
   562 
   563 
   563 \input{Recdef/document/simplification.tex}
   564 \input{Recdef/document/simplification.tex}
   564 
   565 
   565 \subsection{Induction}
   566 \subsection{Induction}
   566 \index{induction!recursion|(}
   567 \index{induction!recursion|(}