src/HOL/NSA/document/root.tex
author huffman
Thu, 03 Jul 2008 17:47:22 +0200
changeset 27468 0783dd1dc13d
child 40945 b8703f63bfb2
permissions -rw-r--r--
move nonstandard analysis theories to NSA directory
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27468
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     1
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     2
% $Id$
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     3
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     4
\documentclass[11pt,a4paper]{article}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     5
\usepackage{graphicx,isabelle,isabellesym,latexsym}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     6
\usepackage[latin1]{inputenc}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     7
\usepackage{pdfsetup}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     8
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
     9
\urlstyle{rm}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    10
\isabellestyle{it}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    11
\pagestyle{myheadings}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    12
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    13
\begin{document}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    14
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    15
\title{Isabelle/HOL-NSA --- Non-Standard Analysis}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    16
\maketitle
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    17
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    18
\tableofcontents
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    19
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    20
\begin{center}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    21
  \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    22
\end{center}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    23
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    24
\newpage
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    25
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    26
\renewcommand{\isamarkupheader}[1]%
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    27
{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    28
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    29
\parindent 0pt\parskip 0.5ex
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    30
\input{session}
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    31
0783dd1dc13d move nonstandard analysis theories to NSA directory
huffman
parents:
diff changeset
    32
\end{document}