diff -r 0502f06c2d29 -r 98d3ca2c18f7 doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Wed Aug 30 14:02:12 2000 +0200
+++ b/doc-src/TutorialI/fp.tex	Wed Aug 30 14:38:48 2000 +0200
@@ -558,29 +558,11 @@
 \input{Misc/document/arith4.tex}%
 is not proved by simplification and requires \isa{arith}.
 
-\subsubsection{Permutative rewrite rules}
-
-A rewrite rule is \textbf{permutative} if the left-hand side and right-hand
-side are the same up to renaming of variables.  The most common permutative
-rule is commutativity: $x+y = y+x$.  Another example is $(x-y)-z = (x-z)-y$.
-Such rules are problematic because once they apply, they can be used forever.
-The simplifier is aware of this danger and treats permutative rules
-separately. For details see~\cite{isabelle-ref}.
-
 \subsubsection{Tracing}
 \indexbold{tracing the simplifier}
 
 {\makeatother\input{Misc/document/trace_simp.tex}}
 
-\subsection{How it works}
-\label{sec:SimpHow}
-
-\subsubsection{Higher-order patterns}
-
-\subsubsection{Local assumptions}
-
-\subsubsection{The preprocessor}
-
 \index{simplification|)}
 
 \section{Induction heuristics}
@@ -800,9 +782,3 @@
 \input{Recdef/document/Nested2.tex}
 
 \index{*recdef|)}
-
-\section{Advanced induction techniques}
-\label{sec:advanced-ind}
-\input{Misc/document/AdvancedInd.tex}
-
-%\input{Datatype/document/Nested2.tex}