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