src/HOL/Real_Asymp/Manual/document/root.tex
author wenzelm
Mon, 11 Sep 2023 19:30:48 +0200
changeset 78659 b5f3d1051b13
parent 73404 299f6a8faccc
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
68677
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     1
\documentclass[11pt,a4paper]{article}
73404
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 68677
diff changeset
     2
\usepackage[T1]{fontenc}
68677
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     3
\usepackage{amsfonts, amsmath, amssymb}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     4
\usepackage{railsetup}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     5
\usepackage{iman}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     6
\usepackage{extra}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     7
\usepackage{isar}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     8
\usepackage{isabelle}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     9
\usepackage{isabellesym}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    10
\usepackage{style}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    11
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    12
% this should be the last package used
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    13
\usepackage{pdfsetup}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    14
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    15
% urls in roman style, theory text in math-similar italics
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    16
\urlstyle{rm}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    17
\isabellestyle{it}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    18
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    19
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    20
\begin{document}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    21
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    22
\title{\texttt{real\_asymp}: Semi-Automatic Real Asymptotics\\ in Isabelle\slash HOL}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    23
\author{Manuel Eberl}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    24
\maketitle
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    25
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    26
\tableofcontents
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    27
\newpage
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    28
\parindent 0pt\parskip 0.5ex
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    29
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    30
\input{session}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    31
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    32
\bibliographystyle{abbrv}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    33
\bibliography{root}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    34
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    35
\end{document}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    36
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    37
%%% Local Variables:
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    38
%%% mode: latex
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    39
%%% TeX-master: t
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    40
%%% End: