diff -r 78822f2d921f -r 67f2920862c7 doc-src/TutorialI/Advanced/advanced.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Advanced/advanced.tex Thu Sep 14 17:46:00 2000 +0200 @@ -0,0 +1,26 @@ +\chapter{Advanced Simplification, Recursion, and Induction} +\markboth{}{CHAPTER 4: ADVANCED} + +Although we have already learned a lot about simplification, recursion and +induction, there are some advanced proof techniques that we have not covered +yet and which are worth knowing about if you intend to beome a serious +(human) theorem prover. The three sections of this chapter are almost +independent of each other and can be read in any order. Only the notion of +\emph{congruence rules}, introduced in the section on simplification, is +required for parts of the section on recursion. + +\input{document/simp.tex} + +\section{Advanced forms of recursion} +\label{sec:advanced-recdef} +\index{*recdef|(} +\input{../Recdef/document/Nested0.tex} +\input{../Recdef/document/Nested1.tex} +\input{../Recdef/document/Nested2.tex} +\index{*recdef|)} + +\section{Advanced induction techniques} +\label{sec:advanced-ind} +\index{induction|(} +\input{../Misc/document/AdvancedInd.tex} +\index{induction|)}