src/HOL/Complex/document/root.tex
author nipkow
Fri, 16 Jul 2004 17:31:54 +0200
changeset 15054 1ad0b310bc54
child 17159 d5060118122e
permissions -rw-r--r--
Created.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15054
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
     1
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
     2
% $Id$
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
     3
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
     4
\documentclass[11pt,a4paper]{article}
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
     5
\usepackage{graphicx,isabelle,isabellesym,latexsym}
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
     6
\usepackage[latin1]{inputenc}
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
     7
\usepackage{pdfsetup}
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
     8
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
     9
\urlstyle{rm}
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    10
\isabellestyle{it}
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    11
\pagestyle{myheadings}
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    12
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    13
\begin{document}
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    14
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    15
\title{Isabelle/HOL-Complex --- Higher-Order Logic with Complex Numbers}
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    16
\maketitle
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    17
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    18
\tableofcontents
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    19
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    20
\begin{center}
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    21
  \includegraphics[scale=0.3]{session_graph}
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    22
\end{center}
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    23
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    24
\newpage
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    25
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    26
\renewcommand{\isamarkupheader}[1]%
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    27
{\section{\isabellecontext: #1}\markright{THEORY~``\isabellecontext''}}
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    28
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    29
\parindent 0pt\parskip 0.5ex
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    30
\input{session}
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    31
1ad0b310bc54 Created.
nipkow
parents:
diff changeset
    32
\end{document}