# HG changeset patch
# User nipkow
# Date 967639550 -7200
# Node ID d18d5c4a1f809532c037c6ef9bf987ec2230a0e3
# Parent  98d3ca2c18f7b023d268fde6dd45fc437457c2f8
*** empty log message ***

diff -r 98d3ca2c18f7 -r d18d5c4a1f80 doc-src/TutorialI/tricks.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/tricks.tex	Wed Aug 30 14:45:50 2000 +0200
@@ -0,0 +1,36 @@
+\chapter{The Tricks of the Trade}
+
+\section{Simplification}
+\index{simplification|(}
+
+\subsection{Advanced features}
+
+\subsubsection{Congruence rules}
+
+
+\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}.
+
+
+
+\subsection{How it works}
+\label{sec:SimpHow}
+
+\subsubsection{Higher-order patterns}
+
+\subsubsection{Local assumptions}
+
+\subsubsection{The preprocessor}
+
+\index{simplification|)}
+
+
+\section{Advanced induction techniques}
+\label{sec:advanced-ind}
+\input{Misc/document/AdvancedInd.tex}