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
huffman@24338
     1
% $Id$
huffman@24338
     2
huffman@24338
     3
\documentclass[11pt,a4paper]{article}
huffman@24338
     4
\usepackage{graphicx,isabelle,isabellesym}
huffman@24338
     5
\usepackage{pdfsetup}
huffman@24338
     6
huffman@24338
     7
\urlstyle{rm}
huffman@24338
     8
\isabellestyle{it}
huffman@24338
     9
\pagestyle{myheadings}
huffman@24338
    10
huffman@24338
    11
\begin{document}
huffman@24338
    12
huffman@24338
    13
\title{Machine Words in Isabelle/HOL}
huffman@24338
    14
kleing@25294
    15
\author{Jeremy Dawson, Paul Graunke, Brian Huffman, Gerwin Klein, and John Matthews}
kleing@25294
    16
huffman@24338
    17
\maketitle
huffman@24338
    18
kleing@25262
    19
\begin{abstract}
kleing@25262
    20
A formalisation of generic, fixed size machine words in Isabelle/HOL. An earlier version of this 
kleing@25262
    21
formalisation is described in \cite{dawson-avocs07}.  
kleing@25262
    22
\end{abstract}
kleing@25262
    23
huffman@24338
    24
\tableofcontents
huffman@24338
    25
huffman@24338
    26
\begin{center}
huffman@24338
    27
  \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
huffman@24338
    28
\end{center}
huffman@24338
    29
huffman@24338
    30
\newpage
huffman@24338
    31
huffman@24338
    32
\renewcommand{\isamarkupheader}[1]%
huffman@24338
    33
{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
huffman@24338
    34
huffman@24338
    35
\parindent 0pt\parskip 0.5ex
huffman@24338
    36
\input{session}
huffman@24338
    37
kleing@25262
    38
\bibliographystyle{plain}
kleing@25262
    39
\bibliography{root}
kleing@25262
    40
huffman@24338
    41
\end{document}