\section{Introduction}

The convenience of proof by term-rewriting is demonstrated by the
theorem provers which rely wholly or primarily upon it
(eg Larch \cite{LP}),
and by the prominent place that rewriting tactics have in provers such as 
Isabelle \cite{Ref} and HOL \cite{HOLdesc}.

The Logic of Partial Functions (LPF) 
handles undefined terms, and is the logic underlying VDM (see \cite{Blikle}).
It has been mechanized in Isabelle by Agerholm \& Frost \cite{agfr}.
Proofs in LPF
could use standard rewriting of equal terms, but this would 
be complicated by the need to prove that
the term to be rewritten is defined, since an undefined term is not 
equal to anything.
In \S\ref{lpf} we demonstrate that this complication can be avoided in LPF 
by using not equality but the partial order $\sqsubseteq$ of
domain theory, or ``replaceability'', as a condition for
rewriting one term by another.

Display Logic \cite{Bel} is
a generalization of the Gentzen sequent calculus.
Several logics have been formalized in it.
Like the sequent calculus, Display Logic 
does not have an explicit notion of equality of subterms.
Therefore, one might imagine that term rewriting would not be available
in Display Logic.
The equivalence relation $\equiv$ which
arises from the standard Lindenbaum algebra 
(as in \cite[\S4]{dRA}) is usually a congruence, as
is normally required for rewriting. 
However this relation is not available in 
Display Logic itself, since it is a meta-level concept.
In \S\ref{dl} we discuss tactics which, effectively, enable rewriting
in Display Logic.

In \S\ref{intl} we consider the features of these logics which make
these tactics possible. We looked for a common thread between
the two methods used (for LPF and for Display Logic), without success.
Rather, \S\ref{intl} shows a contrast between the two methods.

The source files containing the ML functions described are at
\verb|http://arp.anu.edu.au:80/~jeremy/TPHOLs98|