--- a/doc-src/Ref/simplifier.tex Mon Oct 20 11:47:04 1997 +0200
+++ b/doc-src/Ref/simplifier.tex Mon Oct 20 11:53:42 1997 +0200
@@ -1,5 +1,6 @@
%% $Id$
-\chapter{Simplification} \label{simp-chap}
+\chapter{Simplification}
+\label{chap:simplification}
\index{simplification|(}
This chapter describes Isabelle's generic simplification package, which
@@ -177,12 +178,13 @@
{(\Var{i}+\Var{j})+\Var{k}}$ is ok.
It will also deal gracefully with all rules whose left-hand sides are
-so-called {\em higher-order patterns}~\cite{nipkow-patterns}. These are terms
-in $\beta$-normal form (this will always be the case unless you have done
-something strange) where each occurrence of an unknown is of the form
-$\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are distinct bound variables.
-Hence $(\forall x.\Var{P}(x) \land \Var{Q}(x)) \bimp (\forall x.\Var{P}(x))
-\land (\forall x.\Var{Q}(x))$ is also ok, in both directions.
+so-called {\em higher-order patterns}~\cite{nipkow-patterns}.
+\indexbold{higher-order pattern}\indexbold{pattern, higher-order}
+These are terms in $\beta$-normal form (this will always be the case unless
+you have done something strange) where each occurrence of an unknown is of
+the form $\Var{F}(x@1,\dots,x@n)$, where the $x@i$ are distinct bound
+variables. Hence $(\forall x.\Var{P}(x) \land \Var{Q}(x)) \bimp (\forall
+x.\Var{P}(x)) \land (\forall x.\Var{Q}(x))$ is also ok, in both directions.
In some rare cases the rewriter will even deal with quite general rules: for
example ${\Var{f}(\Var{x})\in range(\Var{f})} = True$ rewrites $g(a) \in