author | wenzelm |
Mon, 25 May 2015 22:11:43 +0200 | |
changeset 60301 | ff82ba1893c8 |
parent 60185 | cc71f01f9fde |
parent 60286 | 410115884a92 |
child 60484 | 98ee86354354 |
permissions | -rw-r--r-- |
7836 | 1 |
\documentclass[12pt,a4paper,fleqn]{report} |
60185
cc71f01f9fde
prefer lmodern, which produces scalable T1 fonts even with Debian-ized TeXLive;
wenzelm
parents:
59974
diff
changeset
|
2 |
\usepackage{lmodern} |
55365 | 3 |
\usepackage[T1]{fontenc} |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28773
diff
changeset
|
4 |
\usepackage{amssymb} |
59974
b911c8ba0b69
added symbol for \<hole> (from DejaVuSansMono and DejaVuSansMono-Bold version 2.34);
wenzelm
parents:
57590
diff
changeset
|
5 |
\usepackage{wasysym} |
48171
28a6d67c93f0
default for \<euro> is now based on eurosym package, instead of slightly exotic babel/greek (which causes problems with the Gentoo installation on lxbroy2);
wenzelm
parents:
48057
diff
changeset
|
6 |
\usepackage{eurosym} |
28a6d67c93f0
default for \<euro> is now based on eurosym package, instead of slightly exotic babel/greek (which causes problems with the Gentoo installation on lxbroy2);
wenzelm
parents:
48057
diff
changeset
|
7 |
\usepackage[english]{babel} |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28773
diff
changeset
|
8 |
\usepackage[only,bigsqcap]{stmaryrd} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28773
diff
changeset
|
9 |
\usepackage{textcomp} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28773
diff
changeset
|
10 |
\usepackage{latexsym} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28773
diff
changeset
|
11 |
\usepackage{graphicx} |
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28773
diff
changeset
|
12 |
\let\intorig=\int %iman.sty redefines \int |
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
13 |
\usepackage{iman,extra,isar,proof} |
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
14 |
\usepackage[nohyphen,strings]{underscore} |
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
15 |
\usepackage{isabelle} |
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
16 |
\usepackage{isabellesym} |
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
17 |
\usepackage{railsetup} |
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
18 |
\usepackage{ttbox} |
28773 | 19 |
\usepackage{supertabular} |
26738
615e1a86787b
basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
18021
diff
changeset
|
20 |
\usepackage{style} |
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
21 |
\usepackage{pdfsetup} |
7046 | 22 |
|
26741 | 23 |
\hyphenation{Isabelle} |
24 |
\hyphenation{Isar} |
|
25 |
||
26 |
\isadroptag{theory} |
|
7046 | 27 |
\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual} |
26870 | 28 |
\author{\emph{Makarius Wenzel} \\[3ex] |
29 |
With Contributions by |
|
30 |
Clemens Ballarin, |
|
31 |
Stefan Berghofer, \\ |
|
44966 | 32 |
Jasmin Blanchette, |
30569 | 33 |
Timothy Bourke, |
44966 | 34 |
Lukas Bulwahn, \\ |
50130 | 35 |
Amine Chaieb, |
27038 | 36 |
Lucas Dixon, |
50130 | 37 |
Florian Haftmann, \\ |
38 |
Brian Huffman, |
|
57590 | 39 |
Lars Hupel, |
40 |
Gerwin Klein, \\ |
|
41 |
Alexander Krauss, |
|
50130 | 42 |
Ond\v{r}ej Kun\v{c}ar, |
57590 | 43 |
Andreas Lochbihler, \\ |
44 |
Tobias Nipkow, |
|
56364 | 45 |
Lars Noschinski, |
57590 | 46 |
David von Oheimb, \\ |
47 |
Larry Paulson, |
|
56364 | 48 |
Sebastian Skalberg, |
52896 | 49 |
Christian Sternagel |
26870 | 50 |
} |
7046 | 51 |
|
7050 | 52 |
\makeindex |
53 |
||
18021 | 54 |
\chardef\charbackquote=`\` |
55 |
\newcommand{\backquote}{\mbox{\tt\charbackquote}} |
|
56 |
||
7046 | 57 |
|
58 |
\begin{document} |
|
59 |
||
60 |
\maketitle |
|
61 |
||
42915
f35aae36cad0
turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);
wenzelm
parents:
42632
diff
changeset
|
62 |
\pagenumbering{roman} |
60286 | 63 |
\chapter*{Preface} |
64 |
\input{Preface.tex} |
|
42915
f35aae36cad0
turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);
wenzelm
parents:
42632
diff
changeset
|
65 |
\tableofcontents |
f35aae36cad0
turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);
wenzelm
parents:
42632
diff
changeset
|
66 |
\clearfirst |
7046 | 67 |
|
29718 | 68 |
\part{Basic Concepts} |
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
69 |
\input{Synopsis.tex} |
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
70 |
\input{Framework.tex} |
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
71 |
\input{First_Order_Logic.tex} |
29718 | 72 |
\part{General Language Elements} |
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
73 |
\input{Outer_Syntax.tex} |
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
74 |
\input{Document_Preparation.tex} |
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
75 |
\input{Spec.tex} |
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
76 |
\input{Proof.tex} |
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
77 |
\input{Inner_Syntax.tex} |
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
78 |
\input{Misc.tex} |
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
79 |
\input{Generic.tex} |
50109 | 80 |
\part{Isabelle/HOL}\label{part:hol} |
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
81 |
\input{HOL_Specific.tex} |
7046 | 82 |
|
29718 | 83 |
\part{Appendix} |
7895 | 84 |
\appendix |
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
85 |
\input{Quick_Reference.tex} |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28773
diff
changeset
|
86 |
\let\int\intorig |
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
87 |
\input{Symbols.tex} |
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
88 |
\input{ML_Tactic.tex} |
7895 | 89 |
|
7046 | 90 |
\begingroup |
48057 | 91 |
\tocentry{\bibname} |
30116 | 92 |
\bibliographystyle{abbrv} \small\raggedright\frenchspacing |
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
93 |
\bibliography{manual} |
7046 | 94 |
\endgroup |
95 |
||
48057 | 96 |
\tocentry{\indexname} |
8828 | 97 |
\printindex |
7046 | 98 |
|
99 |
\end{document} |