| author | wenzelm | 
| Wed, 19 May 2021 11:54:58 +0200 | |
| changeset 73740 | c46ff0efa1ce | 
| parent 73404 | 299f6a8faccc | 
| permissions | -rw-r--r-- | 
| 70089 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 1 | \documentclass[11pt,a4paper]{book}
 | 
| 73404 | 2 | \usepackage[T1]{fontenc}
 | 
| 70089 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 3 | \usepackage{graphicx}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 4 | \usepackage{isabelle}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 5 | \usepackage{isabellesym}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 6 | \usepackage{latexsym}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 7 | \usepackage{textcomp}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 8 | \usepackage{amsmath}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 9 | \usepackage{amssymb}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 10 | \usepackage[only,bigsqcap]{stmaryrd}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 11 | \usepackage{pdfsetup}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 12 | |
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 13 | \usepackage{tocloft}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 14 | \setlength{\cftsubsecnumwidth}{3em}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 15 | \cftsetpnumwidth{2em}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 16 | \cftsetrmarg{3em}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 17 | |
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 18 | \urlstyle{rm}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 19 | \isabellestyle{literalunderscore}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 20 | \pagestyle{myheadings}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 21 | |
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 22 | \begin{document}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 23 | |
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 24 | \title{Homology}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 25 | \maketitle | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 26 | |
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 27 | \tableofcontents | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 28 | |
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 29 | \begin{center}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 30 |   \includegraphics[height=\textheight]{session_graph}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 31 | \end{center}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 32 | |
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 33 | \newpage | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 34 | |
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 35 | \renewcommand{\setisabellecontext}[1]{\markright{\href{#1.html}{#1.thy}}}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 36 | |
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 37 | \parindent 0pt\parskip 0.5ex | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 38 | \input{session}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 39 | |
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 40 | \pagestyle{headings}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 41 | \bibliographystyle{abbrv}
 | 
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 42 | |
| 
eca8611201e9
new Homology target, depending on HOL-Algebra and HOL-Analysis
 paulson <lp15@cam.ac.uk> parents: diff
changeset | 43 | \end{document}
 |