| author | nipkow | 
| Thu, 13 Apr 2023 15:36:07 +1000 | |
| changeset 77830 | 0f2baf04b782 | 
| parent 73404 | 299f6a8faccc | 
| permissions | -rw-r--r-- | 
| 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 | 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}
 |