doc-src/TutorialI/Advanced/advanced.tex
author nipkow
Thu Sep 14 17:46:00 2000 +0200 (2000-09-14)
changeset 9958 67f2920862c7
child 9993 c0f7fb6e538e
permissions -rw-r--r--
*** empty log message ***
     1 \chapter{Advanced Simplification, Recursion, and Induction}
     2 \markboth{}{CHAPTER 4: ADVANCED}
     3 
     4 Although we have already learned a lot about simplification, recursion and
     5 induction, there are some advanced proof techniques that we have not covered
     6 yet and which are worth knowing about if you intend to beome a serious
     7 (human) theorem prover. The three sections of this chapter are almost
     8 independent of each other and can be read in any order. Only the notion of
     9 \emph{congruence rules}, introduced in the section on simplification, is
    10 required for parts of the section on recursion.
    11 
    12 \input{document/simp.tex}
    13 
    14 \section{Advanced forms of recursion}
    15 \label{sec:advanced-recdef}
    16 \index{*recdef|(}
    17 \input{../Recdef/document/Nested0.tex}
    18 \input{../Recdef/document/Nested1.tex}
    19 \input{../Recdef/document/Nested2.tex}
    20 \index{*recdef|)}
    21 
    22 \section{Advanced induction techniques}
    23 \label{sec:advanced-ind}
    24 \index{induction|(}
    25 \input{../Misc/document/AdvancedInd.tex}
    26 \index{induction|)}