doc-src/TutorialI/tricks.tex
changeset 9958 67f2920862c7
parent 9957 78822f2d921f
child 9959 4a2ae974043d
     1.1 --- a/doc-src/TutorialI/tricks.tex	Thu Sep 14 17:46:00 2000 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,27 +0,0 @@
     1.4 -%\chapter{The Tricks of the Trade}
     1.5 -\chapter{Advanced Simplification, Recursion, and Induction}
     1.6 -\markboth{}{CHAPTER 4: ADVANCED}
     1.7 -
     1.8 -Although we have already learned a lot about simplification, recursion and
     1.9 -induction, there are some advanced proof techniques that we have not covered
    1.10 -yet and which are worth knowing about if you intend to beome a serious
    1.11 -(human) theorem prover. The three sections of this chapter are almost
    1.12 -independent of each other and can be read in any order. Only the notion of
    1.13 -\emph{congruence rules}, introduced in the section on simplification, is
    1.14 -required for parts of the section on recursion.
    1.15 -
    1.16 -\input{Advanced/document/simp.tex}
    1.17 -
    1.18 -\section{Advanced forms of recursion}
    1.19 -\label{sec:advanced-recdef}
    1.20 -\index{*recdef|(}
    1.21 -\input{Recdef/document/Nested0.tex}
    1.22 -\input{Recdef/document/Nested1.tex}
    1.23 -\input{Recdef/document/Nested2.tex}
    1.24 -\index{*recdef|)}
    1.25 -
    1.26 -\section{Advanced induction techniques}
    1.27 -\label{sec:advanced-ind}
    1.28 -\index{induction|(}
    1.29 -\input{Misc/document/AdvancedInd.tex}
    1.30 -\index{induction|)}