|
1 \documentclass[12pt,a4paper,fleqn]{report} |
|
2 \usepackage{amssymb} |
|
3 \usepackage{eurosym} |
|
4 \usepackage[english]{babel} |
|
5 \usepackage[only,bigsqcap]{stmaryrd} |
|
6 \usepackage{textcomp} |
|
7 \usepackage{latexsym} |
|
8 \usepackage{graphicx} |
|
9 \let\intorig=\int %iman.sty redefines \int |
|
10 \usepackage{iman,extra,isar,proof} |
|
11 \usepackage[nohyphen,strings]{underscore} |
|
12 \usepackage{isabelle} |
|
13 \usepackage{isabellesym} |
|
14 \usepackage{railsetup} |
|
15 \usepackage{ttbox} |
|
16 \usepackage{supertabular} |
|
17 \usepackage{style} |
|
18 \usepackage{pdfsetup} |
|
19 |
|
20 \hyphenation{Isabelle} |
|
21 \hyphenation{Isar} |
|
22 |
|
23 \isadroptag{theory} |
|
24 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual} |
|
25 \author{\emph{Makarius Wenzel} \\[3ex] |
|
26 With Contributions by |
|
27 Clemens Ballarin, |
|
28 Stefan Berghofer, \\ |
|
29 Jasmin Blanchette, |
|
30 Timothy Bourke, |
|
31 Lukas Bulwahn, \\ |
|
32 Lucas Dixon, |
|
33 Florian Haftmann, |
|
34 Brian Huffman, \\ |
|
35 Gerwin Klein, |
|
36 Alexander Krauss, |
|
37 Ond\v{r}ej Kun\v{c}ar, \\ |
|
38 Tobias Nipkow, |
|
39 Lars Noschinski, |
|
40 David von Oheimb, \\ |
|
41 Larry Paulson, |
|
42 Sebastian Skalberg |
|
43 } |
|
44 |
|
45 \makeindex |
|
46 |
|
47 \chardef\charbackquote=`\` |
|
48 \newcommand{\backquote}{\mbox{\tt\charbackquote}} |
|
49 |
|
50 |
|
51 \begin{document} |
|
52 |
|
53 \maketitle |
|
54 |
|
55 \pagenumbering{roman} |
|
56 {\def\isamarkupchapter#1{\chapter*{#1}}\input{Preface.tex}} |
|
57 \tableofcontents |
|
58 \clearfirst |
|
59 |
|
60 \part{Basic Concepts} |
|
61 \input{Synopsis.tex} |
|
62 \input{Framework.tex} |
|
63 \input{First_Order_Logic.tex} |
|
64 \part{General Language Elements} |
|
65 \input{Outer_Syntax.tex} |
|
66 \input{Document_Preparation.tex} |
|
67 \input{Spec.tex} |
|
68 \input{Proof.tex} |
|
69 \input{Inner_Syntax.tex} |
|
70 \input{Misc.tex} |
|
71 \input{Generic.tex} |
|
72 \part{Object-Logic} |
|
73 \input{HOL_Specific.tex} |
|
74 |
|
75 \part{Appendix} |
|
76 \appendix |
|
77 \input{Quick_Reference.tex} |
|
78 \let\int\intorig |
|
79 \input{Symbols.tex} |
|
80 \input{ML_Tactic.tex} |
|
81 |
|
82 \begingroup |
|
83 \tocentry{\bibname} |
|
84 \bibliographystyle{abbrv} \small\raggedright\frenchspacing |
|
85 \bibliography{manual} |
|
86 \endgroup |
|
87 |
|
88 \tocentry{\indexname} |
|
89 \printindex |
|
90 |
|
91 \end{document} |