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% LaTeX master document for abstract spec.
12
13\documentclass[10pt,a4paper]{scrbook}
14
15% These old font commands have been removed from newer versions of
16% the scrbook 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 isabellesym.sty)
28% use only when needed
29\usepackage{amssymb}                   % for \<leadsto>, \<box>, \<diamond>,
30                                       % \<sqsupset>, \<mho>, \<Join>,
31                                       % \<lhd>, \<lesssim>, \<greatersim>,
32                                       % \<lessapprox>, \<greaterapprox>,
33                                       % \<triangleq>, \<yen>, \<lozenge>
34\usepackage[english]{babel}            % greek for \<euro>,
35                                       % english for \<guillemotleft>,
36                                       %             \<guillemotright>
37                                       % default language = last
38%\usepackage[latin1]{inputenc}         % for \<onesuperior>, \<onequarter>,
39                                       % \<twosuperior>, \<onehalf>,
40                                       % \<threesuperior>, \<threequarters>,
41                                       % \<degree>
42%\usepackage[only,bigsqcap]{stmaryrd}  % for \<Sqinter>
43%\usepackage{eufrak}                   % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
44                                       % (only needed if amssymb not used)
45
46\usepackage{graphicx}
47\usepackage[draft]{fixme}
48\usepackage{cite}
49
50% this should be the last package used
51\usepackage{color}
52\definecolor{linkcolor}{rgb}{0,0,0.7}
53\usepackage[colorlinks=true,linkcolor=linkcolor,citecolor=linkcolor,
54            filecolor=linkcolor,pagecolor=linkcolor,urlcolor=linkcolor]{hyperref}
55
56\urlstyle{rm}
57\isabellestyle{tt}
58
59% FIXME: sseefried: change the pdftitle
60\hypersetup
61{
62    pdfauthor={NICTA SSRG Research Group},
63    pdftitle={Bisimlulation proof}
64}
65
66\renewcommand{\isamarkupheader}[1]{\chapter{#1}}
67
68% don't show ML code
69\isadroptag{ML}
70
71% don't show proofs
72\isadroptag{proof}
73
74% do not show confusing double quotes in definitions and lemmas
75%\renewcommand{\isachardoublequote}{}
76%\renewcommand{\isachardoublequoteopen}{}
77%\renewcommand{\isachardoublequoteclose}{}
78
79\parindent 0pt\parskip 0.5ex
80
81\setlength{\oddsidemargin}{0cm}
82\setlength{\evensidemargin}{0cm}
83\setlength{\topmargin}{-1cm}
84\setlength{\textwidth}{15.5cm}
85\setlength{\textheight}{22.5cm}
86
87\newcommand{\meth}[1]{\texttt{#1()}}
88\newcommand{\obj}[1]{\textsf{\small #1}}
89
90\begin{document}
91
92% FIXME: sseefried: Change the title
93\title{Bisimulation Proof}
94
95% FIXME: sseefried: Is this all the authors?
96\author{%
97Simon Winwood \and
98Gerwin Klein \and
99Sean Seefried \and
100}
101
102
103\maketitle
104
105\thispagestyle{empty}
106
107\vfill
108
109\copyright~2013 National ICT Australia Limited.\\
110% FIXME: sseefried: Should we have a copyright for Open Kernel Labs, Inc as well. Uncomment below if so.
111% \copyright~2013 Open Kernel Labs, Inc.\\
112
113% FIXME: sseefried: This license is almost certainly not correct. Change it.
114\textsc{All rights reserved}. This document is made available under
115the terms of the National ICT Australia Limited
116\textsc{Non-Commercial License Agreement} and Open Kernel Labs,
117Inc.\ \textsc{Non-Commercial License Agreement}. Copies of the
118licenses are available in the top-level directory of this
119distribution.
120
121\clearpage
122
123\chapter*{Abstract}
124% FIXME: sseefried: Write an abstract for the document
125%This document is the text version of the abstract, formal
126%Isabelle/HOL specification of the seL4 microkernel. It is
127%intended to give a precise, operational definition of the
128%seL4 microkernel on the ARMv6 architecture.
129%The document contains a short overview, followed by
130%text generated from the formal Isabelle/HOL definitions.
131
132This document is not a tutorial or user manual and is not intended to be read
133as such. Please see the bundled user manual for a higher-level introduction to
134the kernel.
135
136
137\cleardoublepage
138
139\tableofcontents
140
141\input{session}
142
143% \bibliographystyle{plain}
144% \bibliography{defs,root}
145
146\end{document}
147
148%%% Local Variables:
149%%% mode: latex
150%%% TeX-master: t
151%%% End:
152