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