src/HOL/Word/document/root.tex
author kleing
Fri, 02 Nov 2007 12:35:27 +0100
changeset 25262 d0928156e326
parent 24338 14787722149a
child 25294 437d3a414bfa
permissions -rw-r--r--
Added reference to Jeremy Dawson's paper on the word library. Added header to remaining word/*.thy files so they show up in toc.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24338
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     1
% $Id$
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     2
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     3
\documentclass[11pt,a4paper]{article}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     4
\usepackage{graphicx,isabelle,isabellesym}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     5
\usepackage{pdfsetup}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     6
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     7
\urlstyle{rm}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     8
\isabellestyle{it}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
     9
\pagestyle{myheadings}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    10
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    11
\begin{document}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    12
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    13
\title{Machine Words in Isabelle/HOL}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    14
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
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    30
\renewcommand{\isamarkupheader}[1]%
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    31
{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    32
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    33
\parindent 0pt\parskip 0.5ex
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    34
\input{session}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    35
25262
d0928156e326 Added reference to Jeremy Dawson's paper on the word library.
kleing
parents: 24338
diff changeset
    36
\bibliographystyle{plain}
d0928156e326 Added reference to Jeremy Dawson's paper on the word library.
kleing
parents: 24338
diff changeset
    37
\bibliography{root}
d0928156e326 Added reference to Jeremy Dawson's paper on the word library.
kleing
parents: 24338
diff changeset
    38
24338
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    39
\end{document}