\documentstyle[headerfooter,a4,a4wide,notation]{article}
\newcommand{\version}{2 Sep 1992}
\pagestyle{headings}
\pageheaderlinetrue
\pageheader{\sl\rightmark}{\bf\version}{\thepage}
%\pageheader{\sl\rightmark}{}{\thepage}
\pagefooter{}{}{}
%
\title{\huge Action Semantics of {\sc microSpecimen}}
\author{Hermano Moura
\thanks{Supported by CNPq, Brazil. On leave from
    Caixa Econ\^omica Federal, Brazil.}\\
University of Glasgow\\ 
Department of Computing Science\\
Glasgow, G12\ 8QQ, Scotland \\
{\tt moura@dcs.glasgow.ac.uk}\\ \\
\date{2nd September 1992}}
%
\begin{document}
\maketitle
%
\begin{abstract}
\noindent
This document gives the definition of {\sc microSpecimen}, a simple imperative
language designed to serve as an example language in our research on 
semantics-directed compiler generation.
\end{abstract}
%
\tableofcontents
%\newpage
\input{informal}
\input{microspecimen}
\end{document}
