1% 2% Copyright 2014, NICTA 3% 4% This software may be distributed and modified according to the terms of 5% the GNU General Public License version 2. Note that NO WARRANTY is provided. 6% See "LICENSE_GPLv2.txt" for details. 7% 8% @TAG(NICTA_GPL) 9% 10 11\documentclass[11pt,a4paper]{scrreprt} 12 13\newif \ifDraft \Draftfalse 14 15% These old font commands have been removed from newer versions of 16% the scrreprt document class, but isabelle.sty still uses them. 17\DeclareOldFontCommand{\rm}{\normalfont\rmfamily}{\mathrm} 18\DeclareOldFontCommand{\sf}{\normalfont\sffamily}{\mathsf} 19\DeclareOldFontCommand{\tt}{\normalfont\ttfamily}{\mathtt} 20\DeclareOldFontCommand{\bf}{\normalfont\bfseries}{\mathbf} 21\DeclareOldFontCommand{\it}{\normalfont\itshape}{\mathit} 22\DeclareOldFontCommand{\sl}{\normalfont\slshape}{\@nomath\sl} 23\DeclareOldFontCommand{\sc}{\normalfont\scshape}{\@nomath\sc} 24 25\usepackage{isabelle,isabellesym} 26 27% further packages required for unusual symbols (see also 28% isabellesym.sty), use only when needed 29 30%\usepackage{amssymb} 31 %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>, 32 %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>, 33 %\<triangleq>, \<yen>, \<lozenge> 34 35\usepackage[english]{babel} 36 %option greek for \<euro> 37 %option english (default language) for \<guillemotleft>, \<guillemotright> 38 39%\usepackage[only,bigsqcap]{stmaryrd} 40 %for \<Sqinter> 41 42%\usepackage{eufrak} 43 %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb) 44 45%\usepackage{textcomp} 46 %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>, 47 %\<currency> 48 49 50% Extra CAmkES bits. 51\usepackage{graphicx} 52\usepackage{enumerate} 53 54% From ERTOS setup 55\setkeys{Gin}{keepaspectratio=true,clip=true,draft=false,width=\linewidth} 56\usepackage{times,cite,url,fancyhdr,microtype,color,geometry} 57 58\renewcommand{\ttdefault}{cmtt} % CM rather than courier for \tt 59 60\usepackage{xspace} 61\usepackage{listings} 62\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}}} 63 64 65\ifDraft 66\usepackage{draftcopy} 67\newcommand{\Comment}[1]{\textbf{\textsl{#1}}} 68\newcommand{\FIXME}[1]{\textbf{\textsl{FIXME: #1}}} 69\newcommand{\todo}[1]{\textbf{TODO: \textsl{#1}}} 70\date{\small\today} 71\else 72\newcommand{\Comment}[1]{\relax} 73\newcommand{\FIXME}[1]{\relax} 74\newcommand{\todo}[1]{\relax} 75\date{} 76\fi 77 78 79% From camkes manual 80\newcommand{\selfour}{seL4\xspace} 81\newcommand{\Selfour}{SeL4\xspace} 82\newcommand{\camkes}{CAmkES\xspace} 83 84\newcommand{\code}[1]{\texttt{#1}} 85 86 87\newcommand{\titl}{CAmkES Formalisation of a Component Platform} 88\newcommand{\authors}{Matthew Fernandez, Gerwin Klein, Ihor Kuz, Toby Murray} 89 90\definecolor{lcol}{rgb}{0,0,0.5} 91\usepackage[bookmarks,hyperindex,pdftex, 92 colorlinks=true,linkcolor=lcol,citecolor=lcol, 93 filecolor=lcol,urlcolor=lcol, 94 pdfauthor={\authors}, 95 pdftitle={\titl}, 96 plainpages=false]{hyperref} 97 98 99\addto\extrasenglish{% 100\renewcommand{\chapterautorefname}{Chapter} 101\renewcommand{\sectionautorefname}{Section} 102\renewcommand{\subsectionautorefname}{Section} 103\renewcommand{\subsubsectionautorefname}{Section} 104\renewcommand{\appendixautorefname}{Appendix} 105\renewcommand{\Hfootnoteautorefname}{Footnote} 106} 107 108% urls in roman style 109\urlstyle{rm} 110 111\lstset{basicstyle=\small\tt} 112 113% isabelle style 114\isabellestyle{tt} 115 116% for uniform isabelle font size 117\renewcommand{\isastyle}{\isastyleminor} 118 119% Abstract various things that might change. 120\newcommand{\ccode}[1]{\texttt{#1}} 121\newcommand{\isabelletype}[1]{\emph{#1}} 122\newcommand{\isabelleterm}[1]{\emph{#1}} 123 124\renewcommand{\isamarkupheader}[1]{\chapter{#1}} 125\renewcommand{\isamarkupchapter}[1]{\chapter{#1}} 126\renewcommand{\isamarkupsection}[1]{\section{#1}} 127\renewcommand{\isamarkupsubsection}[1]{\section{#1}} 128\renewcommand{\isamarkupsubsubsection}[1]{\subsection{#1}} 129 130\newcommand{\nictafundingacknowledgement}{% 131NICTA 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.} 132 133 134\newcommand{\trdisclaimer}{% 135This material is based on research sponsored by Air Force Research Laboratory 136and the Defense Advanced Research Projects Agency (DARPA) under agreement number 137FA8750-12-9-0179. The U.S. Government is authorized to reproduce and distribute 138reprints for Governmental purposes notwithstanding any copyright notation 139thereon. 140 141The views and conclusions contained herein are those of the authors and should 142not be interpreted as necessarily representing the official policies or 143endorsements, either expressed or implied, of Air Force Research Laboratory, 144the Defense Advanced Research Projects Agency or the U.S.Government.} 145 146\newcommand{\smalldisclaimer}{} 147\newcommand{\bigdisclaimer}{% 148\nictafundingacknowledgement 149 150\vspace{2ex} 151\trdisclaimer} 152 153 154\newcommand{\pgstyle}{% 155\fancyhf{}% 156\renewcommand{\headrulewidth}{0pt}% 157\fancyfoot[C]{}% 158\fancyfoot[L]{\smalldisclaimer}% 159\fancyfoot[R]{\sl\thepage}} 160 161\fancypagestyle{plain}{\pgstyle} 162 163 164\begin{document} 165 166\parindent 0pt\parskip 0.5ex plus 0.2ex minus 0.1ex 167 168%--------- title page 169\newgeometry{left=25mm,right=25mm,top=35mm,bottom=35mm} 170 171\begin{center} 172 \includegraphics[width=0.2\textwidth]{imgs/NICTA_logo} 173\end{center} 174 175\vspace{14ex} 176\textsf{\huge \titl} 177 178%\vspace{2ex} 179%\textsf{\huge \subtitl} 180 181\vspace{4ex} 182\rule{0.85\textwidth}{5pt} 183\vspace{4ex} 184 185{\large \authors 186 187\vspace{2ex} 188April 2014} 189 190\vfill 191{\small 192\bigdisclaimer 193} 194 195\thispagestyle{empty} 196\newpage 197%--------- end title page 198 199\tableofcontents 200 201\input{intro} 202 203% generated text of all theories 204\input{session} 205 206% This document has no references, but Isabelle unconditionally calls bibtex, 207% foolishly expecting me to back up what I'm saying. Fake a bibliography to 208% pacify it. 209\renewcommand{\refname}{} 210\nocite{*} 211\bibliographystyle{abbrv} 212 213\end{document} 214