src/HOL/Analysis/document/root.tex
author wenzelm
Thu, 09 Sep 2021 14:50:26 +0200
changeset 74269 f084d599bb44
parent 73404 299f6a8faccc
permissions -rw-r--r--
clarified set of items with order of addition;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69676
56acd449da41 chapters for analysis manual
immler
parents: 69608
diff changeset
     1
\documentclass[11pt,a4paper]{book}
73404
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 71060
diff changeset
     2
\usepackage[T1]{fontenc}
63497
ef794d2e3754 HOL-Multivariate_Analysis: add amssymb to document generation; reintroduce \nexists (cf d51a0a772094)
hoelzl
parents: 61977
diff changeset
     3
\usepackage{graphicx}
ef794d2e3754 HOL-Multivariate_Analysis: add amssymb to document generation; reintroduce \nexists (cf d51a0a772094)
hoelzl
parents: 61977
diff changeset
     4
\usepackage{isabelle}
ef794d2e3754 HOL-Multivariate_Analysis: add amssymb to document generation; reintroduce \nexists (cf d51a0a772094)
hoelzl
parents: 61977
diff changeset
     5
\usepackage{isabellesym}
ef794d2e3754 HOL-Multivariate_Analysis: add amssymb to document generation; reintroduce \nexists (cf d51a0a772094)
hoelzl
parents: 61977
diff changeset
     6
\usepackage{latexsym}
ef794d2e3754 HOL-Multivariate_Analysis: add amssymb to document generation; reintroduce \nexists (cf d51a0a772094)
hoelzl
parents: 61977
diff changeset
     7
\usepackage{textcomp}
61977
f55f28132128 proper latex setup;
wenzelm
parents: 58877
diff changeset
     8
\usepackage{amsmath}
63497
ef794d2e3754 HOL-Multivariate_Analysis: add amssymb to document generation; reintroduce \nexists (cf d51a0a772094)
hoelzl
parents: 61977
diff changeset
     9
\usepackage{amssymb}
36334
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    10
\usepackage[only,bigsqcap]{stmaryrd}
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    11
\usepackage{pdfsetup}
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    12
69608
2b3a247889f8 tuned document layout;
wenzelm
parents: 69529
diff changeset
    13
\usepackage{tocloft}
71060
295609359b58 tuned toc
nipkow
parents: 69676
diff changeset
    14
\setlength{\cftsubsecnumwidth}{3.5em}
69608
2b3a247889f8 tuned document layout;
wenzelm
parents: 69529
diff changeset
    15
\cftsetpnumwidth{2em}
2b3a247889f8 tuned document layout;
wenzelm
parents: 69529
diff changeset
    16
\cftsetrmarg{3em}
71060
295609359b58 tuned toc
nipkow
parents: 69676
diff changeset
    17
\renewcommand\cftchapafterpnum{\vskip5pt}
295609359b58 tuned toc
nipkow
parents: 69676
diff changeset
    18
\addtolength{\cftsubsecindent}{-1\cftsecindent}% Reduce indent for \subsection
295609359b58 tuned toc
nipkow
parents: 69676
diff changeset
    19
\setlength{\cftsecindent}{0pt}% Remove indent for \section
295609359b58 tuned toc
nipkow
parents: 69676
diff changeset
    20
%\renewcommand{\numberline}[1]{#1~}% More compact but uneven indentation
69608
2b3a247889f8 tuned document layout;
wenzelm
parents: 69529
diff changeset
    21
36334
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    22
\urlstyle{rm}
69517
dc20f278e8f3 tuned style and headers
nipkow
parents: 67143
diff changeset
    23
\isabellestyle{literalunderscore}
36334
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    24
\pagestyle{myheadings}
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    25
71060
295609359b58 tuned toc
nipkow
parents: 69676
diff changeset
    26
\raggedbottom
295609359b58 tuned toc
nipkow
parents: 69676
diff changeset
    27
36334
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    28
\begin{document}
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    29
67143
db609ac2c307 initial version of Analysis document
nipkow
parents: 63627
diff changeset
    30
\title{Analysis}
36334
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    31
\maketitle
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    32
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    33
\tableofcontents
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    34
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    35
\begin{center}
69608
2b3a247889f8 tuned document layout;
wenzelm
parents: 69529
diff changeset
    36
  \includegraphics[height=\textheight]{session_graph}
36334
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    37
\end{center}
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    38
44359
00af710d857e scale dependency graph to fit on page
huffman
parents: 40945
diff changeset
    39
\newpage
00af710d857e scale dependency graph to fit on page
huffman
parents: 40945
diff changeset
    40
69529
4ab9657b3257 capitalize proper names in lemma names
nipkow
parents: 69518
diff changeset
    41
\renewcommand{\setisabellecontext}[1]{\markright{\href{#1.html}{#1.thy}}}
36334
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    42
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    43
\parindent 0pt\parskip 0.5ex
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    44
\input{session}
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    45
69518
bf88364c9e94 tuned headers etc, added bib-file
nipkow
parents: 69517
diff changeset
    46
\pagestyle{headings}
bf88364c9e94 tuned headers etc, added bib-file
nipkow
parents: 69517
diff changeset
    47
\bibliographystyle{abbrv}
bf88364c9e94 tuned headers etc, added bib-file
nipkow
parents: 69517
diff changeset
    48
\bibliography{root}
bf88364c9e94 tuned headers etc, added bib-file
nipkow
parents: 69517
diff changeset
    49
\nocite{dummy}
bf88364c9e94 tuned headers etc, added bib-file
nipkow
parents: 69517
diff changeset
    50
36334
068a01b4bc56 document generation for Multivariate_Analysis
huffman
parents:
diff changeset
    51
\end{document}