%%
%%
\documentclass{llncs}
%\usepackage{makeidx}
%\usepackage{acmnew-xref}

\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{url}

%\RequirePackage{mathptm}
%\RequirePackage{times}
%\RequirePackage{palatino}

\renewcommand{\today}{\number\day\ 
  \ifcase\month\or
  January\or February\or March\or April\or May\or June\or
  July\or August\or September\or October\or November\or December\fi
  \ \number\year}

%\setlength \parskip {1.0ex}
\setcounter{secnumdepth}2
\setcounter{tocdepth}2


\begin{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Preamble

\title{Formalising General Correctness}
\author{Jeremy E. Dawson 
  \thanks{Supported by an Australian Research Council Large Grant}}
\institute{Department of Computer Science \\
Australian National University,
Canberra ACT 0200, Australia \\ 
\url{http://csl.anu.edu.au/~jeremy/} \\
\texttt{jeremy@csl.anu.edu.au} 
%\\[1ex]
%Tel: +61-2-6125-8606 \ \ Fax: +61-2-6125-8651
}

\newcommand\cfile{}
%\renewcommand{\thepage}{\roman{page}}
\newcommand\shrinklist[1]{
\setlength\parskip{#1\parskip}
\setlength\itemsep{#1\itemsep}
\setlength\itemindent{#1\itemindent}
\setlength\topsep{#1\topsep}
}

\newcommand\comment[1]{} 
\newcommand\invrule[2]{ 
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline \hline $ #2 $
  \end{tabular}}
\newcommand\slrule[2]{ % similar to \frac, except
% for use in non-math mode, args interpreted in math mode
  \begin{tabular}{@{}c@{}}
  $ #1 $ \\ \hline $ #2 $
  \end{tabular}}

%\newcommand\proof{\noindent\textbf{Proof.}}
\newcommand\src[1]{source file \texttt{#1}}
\newcommand\apsrc[1]{Appendix \ref{app:code}}
%\newcommand\seesrc[1]{(see source file \texttt{#1}, \apsrc{#1})}
\newcommand\seesrc[1]{(see source file \texttt{#1})}
%\newcommand\insrc[1]{in source file \texttt{#1} (see \apsrc{#1})}
\newcommand\insrc[1]{in source file \texttt{#1}}
\newcommand\page[1]{page~\pageref{#1}}
\newcommand\fig[1]{Fig.~\ref{fig:#1}}
\newcommand\ch[1]{Chapter~\ref{ch:#1}}
\newcommand\tbl[1]{Table~\ref{tbl:#1}}
\newcommand\thrm[1]{Theorem~\ref{thrm:#1}}
\newcommand\lem[1]{Lemma~\ref{lem:#1}}
\newcommand\ttl[1]{\tti{#1}\label{#1}}
\newcommand\ttdl[1]{\texttt{#1}\tti{#1}\label{#1}}
\newcommand\ttdef[1]{\texttt{#1}\tti{#1}}
\newcommand\tti[1]{\index{#1@\texttt{#1}}}
\newcommand\bfi[1]{\textbf{#1}\index{#1|textbf}}
\newcommand\up[1]{\vspace{-#1ex}} 
\newcommand\vpf{\vspace{-3ex}} % to reduce space before proof tree

% automatically defined in LLNCS style
%\newtheorem{thm}{Theorem}%[chapter]
%\newtheorem{lemma}[thm]{Lemma}
%\newtheorem{defn}[thm]{Definition}
%\newtheorem{cor}{Corollary}[thm]
%\renewcommand\thecor{\thethm(\arabic{cor})}

\pagestyle{myheadings}
\pagestyle{plain}

%% Title 
\maketitle

\date{\today}

\begin{abstract}
We consider the abstract command language of Dunne, 
and his account of general correctness. 
We provide an operational interpretation of his abstract commands,
and use the automated theorem proving system Isabelle to prove that 
this operational interpretation leads to Dunne's semantics.
\\[1ex]
Keywords: general correctness, abstract commands.
\end{abstract}

\sloppy 

%\newpage

%% Here begins the main text

\newcommand\file{}

\newcommand\hinput[1]{\renewcommand\file{#1.tex}
  \markboth{\mbox{}\hfill\today\hfill\file}{\today\hfill\file\hfill}
  \input{#1}}

\input{defs}
\input{intro}
\input{mng}
\input{frames}
\input{concl}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Here begins the end matter

% \newpage
\input{bib}

\end{document}