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