%
% Copyright 2014, NICTA
%
% This software may be distributed and modified according to the terms of
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
% See "LICENSE_GPLv2.txt" for details.
%
% @TAG(NICTA_GPL)
%

\documentclass[11pt,a4paper]{scrreprt}

\newif \ifDraft         \Draftfalse

% These old font commands have been removed from newer versions of
% the scrreprt document class, but isabelle.sty still uses them.
\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm}
\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf}
\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt}
\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf}
\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit}
\DeclareOldFontCommand{\sl}{\normalfont\slshape}{\@nomath\sl}
\DeclareOldFontCommand{\sc}{\normalfont\scshape}{\@nomath\sc}

\usepackage{isabelle,isabellesym}

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

%\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

\usepackage[english]{babel}
  %option greek for \<euro>
  %option english (default language) for \<guillemotleft>, \<guillemotright>

%\usepackage[only,bigsqcap]{stmaryrd}
  %for \<Sqinter>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
  %\<currency>


% Extra CAmkES bits.
\usepackage{graphicx}
\usepackage{enumerate}

% From ERTOS setup
\setkeys{Gin}{keepaspectratio=true,clip=true,draft=false,width=\linewidth}
\usepackage{times,cite,url,fancyhdr,microtype,color,geometry}

\renewcommand{\ttdefault}{cmtt}        % CM rather than courier for \tt

\usepackage{xspace}
\usepackage{listings}
\newcommand{\camkeslisting}[1]{{\lstset{basicstyle=\small\ttfamily,keywordstyle=\bf,morekeywords={assembly,component,composition,connection,control,consumes,dataport,emits,event,from,in,inout,int,out,procedure,provides,smallstring,to,uses}}\lstinputlisting{#1}}}


\ifDraft
\usepackage{draftcopy}
\newcommand{\Comment}[1]{\textbf{\textsl{#1}}}
\newcommand{\FIXME}[1]{\textbf{\textsl{FIXME: #1}}}
\newcommand{\todo}[1]{\textbf{TODO: \textsl{#1}}}
\date{\small\today}
\else
\newcommand{\Comment}[1]{\relax}
\newcommand{\FIXME}[1]{\relax}
\newcommand{\todo}[1]{\relax}
\date{}
\fi


% From camkes manual
\newcommand{\selfour}{seL4\xspace}
\newcommand{\Selfour}{SeL4\xspace}
\newcommand{\camkes}{CAmkES\xspace}

\newcommand{\code}[1]{\texttt{#1}}


\newcommand{\titl}{CAmkES Formalisation of a Component Platform}
\newcommand{\authors}{Matthew Fernandez, Gerwin Klein, Ihor Kuz, Toby Murray}

\definecolor{lcol}{rgb}{0,0,0.5}
\usepackage[bookmarks,hyperindex,pdftex,
            colorlinks=true,linkcolor=lcol,citecolor=lcol,
            filecolor=lcol,urlcolor=lcol,
            pdfauthor={\authors},
            pdftitle={\titl},
            plainpages=false]{hyperref}


\addto\extrasenglish{%
\renewcommand{\chapterautorefname}{Chapter}
\renewcommand{\sectionautorefname}{Section}
\renewcommand{\subsectionautorefname}{Section}
\renewcommand{\subsubsectionautorefname}{Section}
\renewcommand{\appendixautorefname}{Appendix}
\renewcommand{\Hfootnoteautorefname}{Footnote}
}

% urls in roman style
\urlstyle{rm}

\lstset{basicstyle=\small\tt}

% isabelle style
\isabellestyle{tt}

% for uniform isabelle font size
\renewcommand{\isastyle}{\isastyleminor}

% Abstract various things that might change.
\newcommand{\ccode}[1]{\texttt{#1}}
\newcommand{\isabelletype}[1]{\emph{#1}}
\newcommand{\isabelleterm}[1]{\emph{#1}}

\renewcommand{\isamarkupheader}[1]{\chapter{#1}}
\renewcommand{\isamarkupchapter}[1]{\chapter{#1}}
\renewcommand{\isamarkupsection}[1]{\section{#1}}
\renewcommand{\isamarkupsubsection}[1]{\section{#1}}
\renewcommand{\isamarkupsubsubsection}[1]{\subsection{#1}}

\newcommand{\nictafundingacknowledgement}{%
NICTA is funded by the Australian Government through the Department of Communications and the Australian Research Council through the ICT Centre of Excellence Program. NICTA is also funded and supported by the Australian Capital Territory, the New South Wales, Queensland and Victorian Governments, the Australian National University, the University of New South Wales, the University of Melbourne, the University of Queensland, the University of Sydney, Griffith University, Queensland University of Technology, Monash University and other university partners.}


\newcommand{\trdisclaimer}{%
This material is based on research sponsored by Air Force Research Laboratory
and the Defense Advanced Research Projects Agency (DARPA) under agreement number
FA8750-12-9-0179. The U.S. Government is authorized to reproduce and distribute
reprints for Governmental purposes notwithstanding any copyright notation
thereon.

The views and conclusions contained herein are those of the authors and should
not be interpreted as necessarily representing the official policies or
endorsements, either expressed or implied, of Air Force Research Laboratory,
the Defense Advanced Research Projects Agency or the U.S.Government.}

\newcommand{\smalldisclaimer}{}
\newcommand{\bigdisclaimer}{%
\nictafundingacknowledgement

\vspace{2ex}
\trdisclaimer}


\newcommand{\pgstyle}{%
\fancyhf{}%
\renewcommand{\headrulewidth}{0pt}%
\fancyfoot[C]{}%
\fancyfoot[L]{\smalldisclaimer}%
\fancyfoot[R]{\sl\thepage}}

\fancypagestyle{plain}{\pgstyle}


\begin{document}

\parindent 0pt\parskip 0.5ex plus 0.2ex minus 0.1ex

%--------- title page
\newgeometry{left=25mm,right=25mm,top=35mm,bottom=35mm}

\begin{center}
 \includegraphics[width=0.2\textwidth]{imgs/NICTA_logo}
\end{center}

\vspace{14ex}
\textsf{\huge \titl}

%\vspace{2ex}
%\textsf{\huge \subtitl}

\vspace{4ex}
\rule{0.85\textwidth}{5pt}
\vspace{4ex}

{\large \authors

\vspace{2ex}
April 2014}

\vfill
{\small
\bigdisclaimer
}

\thispagestyle{empty}
\newpage
%--------- end title page

\tableofcontents

\input{intro}

% generated text of all theories
\input{session}

% This document has no references, but Isabelle unconditionally calls bibtex,
% foolishly expecting me to back up what I'm saying. Fake a bibliography to
% pacify it.
\renewcommand{\refname}{}
\nocite{*}
\bibliographystyle{abbrv}

\end{document}
