\subsection{Isabelle code for Display Logic Rewriting}
  \label{app:DL-code}
The record type \texttt{$\alpha$~meth} has the following fields 
(note that here the arguments referred to as ``actions'' do \emph{not}
have the \texttt{Act} prefix):
\begin{description} %\shrinklist{0.5}
\item[\mdseries\texttt{idact : int -> thm -> $\alpha$}]
is the identity action,
the action which doesn't change the sequent
\item[\mdseries\texttt{actcomb
: (int -> thm -> $\alpha$) * (int -> thm -> $\alpha$) -> 
  (int -> thm -> $\alpha$)}]
is the sequential composition of two actions
\item[\mdseries\texttt{dpact : thm -> int -> thm -> $\alpha$}]
gives the action to be taken to transform a term
using a given display postulate 
\item[\mdseries\texttt{find\_tm : int -> thm -> term}]
is the function which finds the term being
examined, ie, in backwards proof, the subgoal,
or, in forward proof, the conclusion of the theorem.
\end{description}

The source code defining the values used for these arguments is
\begin{center}
\begin{tabular}{l}
\textbf{\qquad \qquad for backward proof} \\ \\
\texttt{fun idact sg = all\_tac ;} \\
\texttt{val actcomb = op THENEXP ;} \\
\texttt{val dpact = rtac o md2 ;} \\
\texttt{fun find\_tm sg state = nth (prems\_of state, sg-1) ;}
%\end{tabular} \end{center} \begin{center} \begin{tabular}{l}
\\ \\
\textbf{\qquad \qquad for forward proof} \\ \\
\texttt{fun idact \_ th = th ;} \\
\texttt{fun actcomb (f, g) \_ = (g 0) o (f 0) ;} \\
\texttt{fun dpact theq \_ th = th RS md1 theq ;} \\
\texttt{fun find\_tm \_ = concl\_of ;}
\end{tabular}
\end{center}

In the above, \texttt{md1} and 
\texttt{md2} turn a meta-equivalence to
forwards and backwards meta-implications;
\verb:(:\textit{tacf1} \verb:THENEXP: \textit{tacf2}\verb:): \textit{sg}
applies \textit{tacf1}
to subgoal number \textit{sg}, then
applies \textit{tacf2} to each resulting subgoal.
This tactical may be generally useful; it corresponds to
the HOL tactical \texttt{THEN} (\cite{HOLdesc}, \S14.4.4),
and to the tactical
\ttdef{THEN\_ALL\_NEW\_SUBGOALS}
as described by Easthaughffe et al in \cite{dove}, p.~378.