src/HOL/Word/document/root.tex
author wenzelm
Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787 64b47495676d
parent 65268 75f2aa8ecb12
permissions -rw-r--r--
obsolete;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24338
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     1
\documentclass[11pt,a4paper]{article}
65268
75f2aa8ecb12 misc tuning and modernization;
wenzelm
parents: 58874
diff changeset
     2
\usepackage{graphicx,isabelle,isabellesym,amssymb}
24338
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     3
\usepackage{pdfsetup}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     4
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     5
\urlstyle{rm}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     6
\isabellestyle{it}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     7
\pagestyle{myheadings}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     8
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     9
\begin{document}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    10
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    11
\title{Machine Words in Isabelle/HOL}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    12
25294
437d3a414bfa acknowledge authors
kleing
parents: 25262
diff changeset
    13
\author{Jeremy Dawson, Paul Graunke, Brian Huffman, Gerwin Klein, and John Matthews}
437d3a414bfa acknowledge authors
kleing
parents: 25262
diff changeset
    14
24338
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    15
\maketitle
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    16
25262
d0928156e326 Added reference to Jeremy Dawson's paper on the word library.
kleing
parents: 24338
diff changeset
    17
\begin{abstract}
d0928156e326 Added reference to Jeremy Dawson's paper on the word library.
kleing
parents: 24338
diff changeset
    18
A formalisation of generic, fixed size machine words in Isabelle/HOL. An earlier version of this 
d0928156e326 Added reference to Jeremy Dawson's paper on the word library.
kleing
parents: 24338
diff changeset
    19
formalisation is described in \cite{dawson-avocs07}.  
d0928156e326 Added reference to Jeremy Dawson's paper on the word library.
kleing
parents: 24338
diff changeset
    20
\end{abstract}
d0928156e326 Added reference to Jeremy Dawson's paper on the word library.
kleing
parents: 24338
diff changeset
    21
24338
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    22
\tableofcontents
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    23
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    24
\begin{center}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    25
  \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    26
\end{center}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    27
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    28
\newpage
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    29
58874
7172c7ffb047 modernized header;
wenzelm
parents: 36862
diff changeset
    30
\renewcommand{\setisabellecontext}[1]{\markright{THEORY~``#1''}}
24338
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    31
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    32
\parindent 0pt\parskip 0.5ex
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    33
\input{session}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    34
25262
d0928156e326 Added reference to Jeremy Dawson's paper on the word library.
kleing
parents: 24338
diff changeset
    35
\bibliographystyle{plain}
d0928156e326 Added reference to Jeremy Dawson's paper on the word library.
kleing
parents: 24338
diff changeset
    36
\bibliography{root}
d0928156e326 Added reference to Jeremy Dawson's paper on the word library.
kleing
parents: 24338
diff changeset
    37
24338
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    38
\end{document}