src/HOL/Word/document/root.tex
author wenzelm
Sat, 29 Sep 2007 21:39:44 +0200
changeset 24759 b448f94b1c88
parent 24338 14787722149a
child 25262 d0928156e326
permissions -rw-r--r--
fixed metis proof (Why did it stop working?);
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}