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}