% 
%	From file `TQfulltemplate.tex',  %Z% %E% %I% %M%
\documentstyle[hol1,11pt,TQ]{article}
\ftlinepenalty=15000
\def\Hide#1{}
\def\Bool{``$\it{:}bool\,$''}
\makeindex
\TPPproject{FST PROJECT}  %% Mandatory field
%\TPPvolume{}
%\TPPpart{}
\TPPtitle{Proof support for Z via HOL (II)}  %% Mandatory field
\TPPref{DS/FMU/RBJ/178}  %% Mandatory field
\def\SCCSversion{%I%
}
\TPPissue{\SCCSversion}  %% Mandatory field
\TPPdate{1990-07-11} %% Mandatory field (with sensible default
\TPPstatus{Draft}			%% Mandatory field
\TPPtype{Specification}
\TPPkeywords{Z HOL}
\TPPauthor{R.B.~Jones & WIN01}  %% Mandatory field
%\TPPauthors{Name 1&location 1\\Name 2&location 2\\Name 3&location 3}
\TPPauthorisation{R.B.~Jones & HAT Manager}
\TPPabstract{
More overheads for Z in HOL presentations.}
%\TPPabstractB{}
%\TPPabstractC{}
%\TPPabstractD{}
%\TPPabstractE{}
%\TPPabstractF{}
\TPPdistribution{\parbox[t]{4.0in}{%
      R.D. Arthan \\ R.B. Jones  
}}

\TPPclass{}
%\def\TPPheadlhs{}
%\def\TPPheadcentre{}
%def\TPPheadrhs{}
%\def\TPPfootlhs{}
%\def\TPPfootcentre{}
%\def\TPPfootrhs{}

\begin{document}
\TPPsetsizes
\makeTPPfrontpage

\vfill
\begin{centering}

\bf Copyright \copyright\ : International Computers Ltd \number\year

\end{centering}

\newpage
\begin{figure}[h]
\special{psfile=178f1.ps}
\end{figure}

\newpage
\begin{figure}[h]
\special{psfile=178f2.ps}
\end{figure}

\newpage
{\center\huge

\vfill

MJCG - HOL

\vfill

change primitives

\vfill

partiality

\vfill

relativisation

\vfill

MPF - HOL

(ref: IDENTITY \& EXISTENCE in INTUITIONISTIC HIGHER ORDER LOGIC)

\vfill

schema types

\vfill

exotic binding constructs

\vfill

decorative conventions

\vfill

Z

\vfill

}
\end{document}

