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