src/HOL/Word/document/root.tex
author haftmann
Tue, 30 Oct 2007 12:14:23 +0100
changeset 25237 5dbb6d583adc
parent 24338 14787722149a
child 25262 d0928156e326
permissions -rw-r--r--
improved website integration
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
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    17
\tableofcontents
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    18
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    19
\begin{center}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    20
  \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    21
\end{center}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    22
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    23
\newpage
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    24
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    25
\renewcommand{\isamarkupheader}[1]%
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    26
{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    27
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    28
\parindent 0pt\parskip 0.5ex
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    29
\input{session}
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    30
14787722149a new root.tex for HOL-Word
huffman
parents:
diff changeset
    31
\end{document}