src/HOL/Complex_Analysis/document/root.tex
author wenzelm
Tue, 09 Mar 2021 21:11:05 +0100
changeset 73404 299f6a8faccc
parent 71189 954ee5acaae0
permissions -rw-r--r--
proper type-setting of cartouches (requires T1); \usepackage[T1]{fontenc} is default for mkroot; \usepackage[utf8]{inputenc} is obsolete in lualatex;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
71189
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     1
\documentclass[11pt,a4paper]{article}
73404
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 71189
diff changeset
     2
\usepackage[T1]{fontenc}
71189
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     3
\usepackage{graphicx}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     4
\usepackage{isabelle}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     5
\usepackage{isabellesym}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     6
\usepackage{latexsym}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     7
\usepackage{textcomp}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     8
\usepackage{amsmath}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
     9
\usepackage{amssymb}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    10
\usepackage[only,bigsqcap]{stmaryrd}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    11
\usepackage{pdfsetup}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    12
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    13
\usepackage{tocloft}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    14
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    15
\urlstyle{rm}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    16
\isabellestyle{literalunderscore}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    17
\pagestyle{myheadings}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    18
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    19
\raggedbottom
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    20
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    21
\begin{document}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    22
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    23
\title{Complex Analysis}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    24
\maketitle
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    25
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    26
\tableofcontents
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    27
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    28
\begin{center}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    29
  \includegraphics[height=\textheight]{session_graph}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    30
\end{center}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    31
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    32
\newpage
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    33
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    34
\renewcommand{\setisabellecontext}[1]{\markright{\href{#1.html}{#1.thy}}}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    35
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    36
\parindent 0pt\parskip 0.5ex
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    37
\input{session}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    38
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    39
\pagestyle{headings}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    40
\bibliographystyle{abbrv}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    41
\bibliography{root}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    42
\nocite{dummy}
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    43
954ee5acaae0 Split off new HOL-Complex_Analysis session from HOL-Analysis
Manuel Eberl <eberlm@in.tum.de>
parents:
diff changeset
    44
\end{document}