src/HOL/Word/document/root.tex
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 25294 437d3a414bfa
child 36862 952b2b102a0a
permissions -rw-r--r--
added lemmas
     1 % $Id$
     2 
     3 \documentclass[11pt,a4paper]{article}
     4 \usepackage{graphicx,isabelle,isabellesym}
     5 \usepackage{pdfsetup}
     6 
     7 \urlstyle{rm}
     8 \isabellestyle{it}
     9 \pagestyle{myheadings}
    10 
    11 \begin{document}
    12 
    13 \title{Machine Words in Isabelle/HOL}
    14 
    15 \author{Jeremy Dawson, Paul Graunke, Brian Huffman, Gerwin Klein, and John Matthews}
    16 
    17 \maketitle
    18 
    19 \begin{abstract}
    20 A formalisation of generic, fixed size machine words in Isabelle/HOL. An earlier version of this 
    21 formalisation is described in \cite{dawson-avocs07}.  
    22 \end{abstract}
    23 
    24 \tableofcontents
    25 
    26 \begin{center}
    27   \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
    28 \end{center}
    29 
    30 \newpage
    31 
    32 \renewcommand{\isamarkupheader}[1]%
    33 {\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
    34 
    35 \parindent 0pt\parskip 0.5ex
    36 \input{session}
    37 
    38 \bibliographystyle{plain}
    39 \bibliography{root}
    40 
    41 \end{document}