src/HOL/Real_Asymp/Manual/document/root.tex
author wenzelm
Mon, 01 Oct 2018 12:41:35 +0200
changeset 69099 d44cb8a3e5e0
parent 68677 99b1cf1e2d48
child 73404 299f6a8faccc
permissions -rw-r--r--
HOL-SPARK .prv files are no longer written to the file-system;
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}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     2
\usepackage{amsfonts, amsmath, amssymb}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     3
\usepackage{railsetup}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     4
\usepackage{iman}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     5
\usepackage{extra}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     6
\usepackage{isar}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     7
\usepackage{isabelle}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     8
\usepackage{isabellesym}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
     9
\usepackage{style}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    10
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    11
% this should be the last package used
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    12
\usepackage{pdfsetup}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    13
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    14
% urls in roman style, theory text in math-similar italics
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    15
\urlstyle{rm}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    16
\isabellestyle{it}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    17
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
\begin{document}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    20
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    21
\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
    22
\author{Manuel Eberl}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    23
\maketitle
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    24
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    25
\tableofcontents
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    26
\newpage
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    27
\parindent 0pt\parskip 0.5ex
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    28
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    29
\input{session}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    30
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    31
\bibliographystyle{abbrv}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    32
\bibliography{root}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    33
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    34
\end{document}
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    35
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    36
%%% Local Variables:
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    37
%%% mode: latex
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    38
%%% TeX-master: t
99b1cf1e2d48 Moved Real_Asymp manual
eberlm <eberlm@in.tum.de>
parents:
diff changeset
    39
%%% End: