| author | blanchet |
| Tue, 30 Apr 2013 10:07:41 +0200 | |
| changeset 51828 | 67c6d6136915 |
| parent 50130 | 8c6fde547cba |
| child 52896 | 73e32ed924b3 |
| permissions | -rw-r--r-- |
| 7836 | 1 |
\documentclass[12pt,a4paper,fleqn]{report}
|
|
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28773
diff
changeset
|
2 |
\usepackage{amssymb}
|
|
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
|
3 |
\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
|
4 |
\usepackage[english]{babel}
|
|
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28773
diff
changeset
|
5 |
\usepackage[only,bigsqcap]{stmaryrd}
|
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28773
diff
changeset
|
6 |
\usepackage{textcomp}
|
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28773
diff
changeset
|
7 |
\usepackage{latexsym}
|
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28773
diff
changeset
|
8 |
\usepackage{graphicx}
|
|
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28773
diff
changeset
|
9 |
\let\intorig=\int %iman.sty redefines \int |
|
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
10 |
\usepackage{iman,extra,isar,proof}
|
|
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
11 |
\usepackage[nohyphen,strings]{underscore}
|
|
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
12 |
\usepackage{isabelle}
|
|
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
13 |
\usepackage{isabellesym}
|
|
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
14 |
\usepackage{railsetup}
|
|
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
15 |
\usepackage{ttbox}
|
| 28773 | 16 |
\usepackage{supertabular}
|
|
26738
615e1a86787b
basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
18021
diff
changeset
|
17 |
\usepackage{style}
|
|
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
18 |
\usepackage{pdfsetup}
|
| 7046 | 19 |
|
| 26741 | 20 |
\hyphenation{Isabelle}
|
21 |
\hyphenation{Isar}
|
|
22 |
||
23 |
\isadroptag{theory}
|
|
| 7046 | 24 |
\title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
|
| 26870 | 25 |
\author{\emph{Makarius Wenzel} \\[3ex]
|
26 |
With Contributions by |
|
27 |
Clemens Ballarin, |
|
28 |
Stefan Berghofer, \\ |
|
| 44966 | 29 |
Jasmin Blanchette, |
| 30569 | 30 |
Timothy Bourke, |
| 44966 | 31 |
Lukas Bulwahn, \\ |
| 50130 | 32 |
Amine Chaieb, |
| 27038 | 33 |
Lucas Dixon, |
| 50130 | 34 |
Florian Haftmann, \\ |
35 |
Brian Huffman, |
|
| 47860 | 36 |
Gerwin Klein, |
| 50130 | 37 |
Alexander Krauss, \\ |
38 |
Ond\v{r}ej Kun\v{c}ar,
|
|
| 44966 | 39 |
Tobias Nipkow, |
| 50130 | 40 |
Lars Noschinski, \\ |
41 |
David von Oheimb, |
|
| 27038 | 42 |
Larry Paulson, |
| 44966 | 43 |
Sebastian Skalberg |
| 26870 | 44 |
} |
| 7046 | 45 |
|
| 7050 | 46 |
\makeindex |
47 |
||
| 18021 | 48 |
\chardef\charbackquote=`\` |
49 |
\newcommand{\backquote}{\mbox{\tt\charbackquote}}
|
|
50 |
||
| 7046 | 51 |
|
52 |
\begin{document}
|
|
53 |
||
54 |
\maketitle |
|
55 |
||
|
42915
f35aae36cad0
turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);
wenzelm
parents:
42632
diff
changeset
|
56 |
\pagenumbering{roman}
|
|
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
57 |
{\def\isamarkupchapter#1{\chapter*{#1}}\input{Preface.tex}}
|
|
42915
f35aae36cad0
turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);
wenzelm
parents:
42632
diff
changeset
|
58 |
\tableofcontents |
|
f35aae36cad0
turned "Overview" into "Preface" (similar to doc-src/Intro/intro.tex);
wenzelm
parents:
42632
diff
changeset
|
59 |
\clearfirst |
| 7046 | 60 |
|
| 29718 | 61 |
\part{Basic Concepts}
|
|
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
62 |
\input{Synopsis.tex}
|
|
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
63 |
\input{Framework.tex}
|
|
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
64 |
\input{First_Order_Logic.tex}
|
| 29718 | 65 |
\part{General Language Elements}
|
|
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
66 |
\input{Outer_Syntax.tex}
|
|
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
67 |
\input{Document_Preparation.tex}
|
|
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
68 |
\input{Spec.tex}
|
|
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
69 |
\input{Proof.tex}
|
|
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
70 |
\input{Inner_Syntax.tex}
|
|
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
71 |
\input{Misc.tex}
|
|
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
72 |
\input{Generic.tex}
|
| 50109 | 73 |
\part{Isabelle/HOL}\label{part:hol}
|
|
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
74 |
\input{HOL_Specific.tex}
|
| 7046 | 75 |
|
| 29718 | 76 |
\part{Appendix}
|
| 7895 | 77 |
\appendix |
|
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
78 |
\input{Quick_Reference.tex}
|
|
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28773
diff
changeset
|
79 |
\let\int\intorig |
|
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
80 |
\input{Symbols.tex}
|
|
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
81 |
\input{ML_Tactic.tex}
|
| 7895 | 82 |
|
| 7046 | 83 |
\begingroup |
| 48057 | 84 |
\tocentry{\bibname}
|
| 30116 | 85 |
\bibliographystyle{abbrv} \small\raggedright\frenchspacing
|
|
48958
12afbf6eb7f9
more standard document preparation within session context;
wenzelm
parents:
48957
diff
changeset
|
86 |
\bibliography{manual}
|
| 7046 | 87 |
\endgroup |
88 |
||
| 48057 | 89 |
\tocentry{\indexname}
|
| 8828 | 90 |
\printindex |
| 7046 | 91 |
|
92 |
\end{document}
|