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|)}