# HG changeset patch
# User nipkow
# Date 877341222 -7200
# Node ID e9d5bcae8351789413d575a8d242aa0a75abea1f
# Parent  c60ff6d0a6b8295a09ea02c876a3318f110fd5a4
\label{simp-chap} -> chap:simplification
Indexed "higher-order pattern"

diff -r c60ff6d0a6b8 -r e9d5bcae8351 doc-src/Ref/ref.ind
--- a/doc-src/Ref/ref.ind	Mon Oct 20 11:47:04 1997 +0200
+++ b/doc-src/Ref/ref.ind	Mon Oct 20 11:53:42 1997 +0200
@@ -313,6 +313,7 @@
   \indexspace
 
   \item {\tt has_fewer_prems}, \bold{32}
+  \item higher-order pattern, \bold{102}
   \item {\tt hyp_subst_tac}, \bold{96}
   \item {\tt hyp_subst_tacs}, \bold{130}
   \item {\tt HypsubstFun}, 97, 130
@@ -427,6 +428,7 @@
   \item {\tt parse_ast_translation}, 91
   \item {\tt parse_rules}, 86
   \item {\tt parse_translation}, 91
+  \item pattern, higher-order, \bold{102}
   \item {\tt pause_tac}, \bold{25}
   \item Poly/{\ML} compiler, 5
   \item {\tt pop_proof}, \bold{14}
diff -r c60ff6d0a6b8 -r e9d5bcae8351 doc-src/Ref/ref.tex
--- a/doc-src/Ref/ref.tex	Mon Oct 20 11:47:04 1997 +0200
+++ b/doc-src/Ref/ref.tex	Mon Oct 20 11:53:42 1997 +0200
@@ -21,7 +21,8 @@
         \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
         With Contributions by Tobias Nipkow and Markus Wenzel%
 \thanks{Tobias Nipkow, of T. U. Munich, wrote most of
-  Chapters~\protect\ref{Defining-Logics} and~\protect\ref{simp-chap}, and part of
+  Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification},
+  and part of
   Chapter~\protect\ref{theories}.  Carsten Clasohm also contributed to
   Chapter~\protect\ref{theories}.  Markus Wenzel contributed to
   Chapter~\protect\ref{chap:syntax}.  Sara Kalvala, Martin Simons and others
diff -r c60ff6d0a6b8 -r e9d5bcae8351 doc-src/Ref/simplifier.tex
--- 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
diff -r c60ff6d0a6b8 -r e9d5bcae8351 doc-src/Ref/substitution.tex
--- a/doc-src/Ref/substitution.tex	Mon Oct 20 11:47:04 1997 +0200
+++ b/doc-src/Ref/substitution.tex	Mon Oct 20 11:53:42 1997 +0200
@@ -15,7 +15,7 @@
 corresponding instances of~$u$, and continues until it reaches a normal
 form.  Substitution handles `one-off' replacements by particular
 equalities while rewriting handles general equations.
-Chapter~\ref{simp-chap} discusses Isabelle's rewriting tactics.
+Chapter~\ref{chap:simplification} discusses Isabelle's rewriting tactics.
 
 
 \section{Substitution rules}
@@ -136,7 +136,7 @@
 Thus, the functor requires the following items:
 \begin{ttdescription}
 \item[Simplifier] should be an instance of the simplifier (see
-  Chapter~\ref{simp-chap}).
+  Chapter~\ref{chap:simplification}).
 
 \item[\ttindexbold{dest_eq}] should return the pair~$(t,u)$ when
 applied to the \ML{} term that represents~$t=u$.  For other terms, it
diff -r c60ff6d0a6b8 -r e9d5bcae8351 doc-src/Ref/tactic.tex
--- a/doc-src/Ref/tactic.tex	Mon Oct 20 11:47:04 1997 +0200
+++ b/doc-src/Ref/tactic.tex	Mon Oct 20 11:53:42 1997 +0200
@@ -7,8 +7,8 @@
 expressed using basic tactics and tacticals.
 
 This chapter only presents the primitive tactics.  Substantial proofs require
-the power of simplification (Chapter~\ref{simp-chap}) and classical reasoning
-(Chapter~\ref{chap:classical}).
+the power of simplification (Chapter~\ref{chap:simplification}) and classical
+reasoning (Chapter~\ref{chap:classical}).
 
 \section{Resolution and assumption tactics}
 {\bf Resolution} is Isabelle's basic mechanism for refining a subgoal using