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