1.1 --- a/doc-src/Ref/ref.ind	Mon Oct 20 11:47:04 1997 +0200
     1.2 +++ b/doc-src/Ref/ref.ind	Mon Oct 20 11:53:42 1997 +0200
     1.3 @@ -313,6 +313,7 @@
     1.4    \indexspace
     1.5  
     1.6    \item {\tt has_fewer_prems}, \bold{32}
     1.7 +  \item higher-order pattern, \bold{102}
     1.8    \item {\tt hyp_subst_tac}, \bold{96}
     1.9    \item {\tt hyp_subst_tacs}, \bold{130}
    1.10    \item {\tt HypsubstFun}, 97, 130
    1.11 @@ -427,6 +428,7 @@
    1.12    \item {\tt parse_ast_translation}, 91
    1.13    \item {\tt parse_rules}, 86
    1.14    \item {\tt parse_translation}, 91
    1.15 +  \item pattern, higher-order, \bold{102}
    1.16    \item {\tt pause_tac}, \bold{25}
    1.17    \item Poly/{\ML} compiler, 5
    1.18    \item {\tt pop_proof}, \bold{14}

     2.1 --- a/doc-src/Ref/ref.tex	Mon Oct 20 11:47:04 1997 +0200
     2.2 +++ b/doc-src/Ref/ref.tex	Mon Oct 20 11:53:42 1997 +0200
     2.3 @@ -21,7 +21,8 @@
     2.4          \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
     2.5          With Contributions by Tobias Nipkow and Markus Wenzel%
     2.6  \thanks{Tobias Nipkow, of T. U. Munich, wrote most of
     2.7 -  Chapters~\protect\ref{Defining-Logics} and~\protect\ref{simp-chap}, and part of
     2.8 +  Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification},
     2.9 +  and part of
    2.10    Chapter~\protect\ref{theories}.  Carsten Clasohm also contributed to
    2.11    Chapter~\protect\ref{theories}.  Markus Wenzel contributed to
    2.12    Chapter~\protect\ref{chap:syntax}.  Sara Kalvala, Martin Simons and others

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

     4.1 --- a/doc-src/Ref/substitution.tex	Mon Oct 20 11:47:04 1997 +0200
     4.2 +++ b/doc-src/Ref/substitution.tex	Mon Oct 20 11:53:42 1997 +0200
     4.3 @@ -15,7 +15,7 @@
     4.4  corresponding instances of~$u$, and continues until it reaches a normal
     4.5  form.  Substitution handles `one-off' replacements by particular
     4.6  equalities while rewriting handles general equations.
     4.7 -Chapter~\ref{simp-chap} discusses Isabelle's rewriting tactics.
     4.8 +Chapter~\ref{chap:simplification} discusses Isabelle's rewriting tactics.
     4.9  
    4.10  
    4.11  \section{Substitution rules}
    4.12 @@ -136,7 +136,7 @@
    4.13  Thus, the functor requires the following items:
    4.14  \begin{ttdescription}
    4.15  \item[Simplifier] should be an instance of the simplifier (see
    4.16 -  Chapter~\ref{simp-chap}).
    4.17 +  Chapter~\ref{chap:simplification}).
    4.18  
    4.19  \item[\ttindexbold{dest_eq}] should return the pair~$(t,u)$ when
    4.20  applied to the \ML{} term that represents~$t=u$.  For other terms, it

     5.1 --- a/doc-src/Ref/tactic.tex	Mon Oct 20 11:47:04 1997 +0200
     5.2 +++ b/doc-src/Ref/tactic.tex	Mon Oct 20 11:53:42 1997 +0200
     5.3 @@ -7,8 +7,8 @@
     5.4  expressed using basic tactics and tacticals.
     5.5  
     5.6  This chapter only presents the primitive tactics.  Substantial proofs require
     5.7 -the power of simplification (Chapter~\ref{simp-chap}) and classical reasoning
     5.8 -(Chapter~\ref{chap:classical}).
     5.9 +the power of simplification (Chapter~\ref{chap:simplification}) and classical
    5.10 +reasoning (Chapter~\ref{chap:classical}).
    5.11  
    5.12  \section{Resolution and assumption tactics}
    5.13  {\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using