equal
deleted
inserted
replaced
1 |
|
2 %% $Id$ |
|
3 |
|
4 \documentclass[12pt,a4paper,fleqn]{report} |
1 \documentclass[12pt,a4paper,fleqn]{report} |
5 \usepackage{latexsym,graphicx} |
2 \usepackage{latexsym,graphicx} |
6 \usepackage[refpage]{nomencl} |
3 \usepackage[refpage]{nomencl} |
7 \usepackage{../iman,../extra,../isar,../proof} |
4 \usepackage{../iman,../extra,../isar,../proof} |
8 \usepackage[nohyphen,strings]{../underscore} |
5 \usepackage[nohyphen,strings]{../underscore} |
20 \author{\emph{Makarius Wenzel} \\[3ex] |
17 \author{\emph{Makarius Wenzel} \\[3ex] |
21 With Contributions by |
18 With Contributions by |
22 Florian Haftmann |
19 Florian Haftmann |
23 and Larry Paulson |
20 and Larry Paulson |
24 } |
21 } |
25 |
|
26 %FIXME |
|
27 %\makeglossary |
|
28 |
22 |
29 \makeindex |
23 \makeindex |
30 |
24 |
31 |
25 |
32 \begin{document} |
26 \begin{document} |
69 \pagenumbering{roman} |
63 \pagenumbering{roman} |
70 \tableofcontents |
64 \tableofcontents |
71 \listoffigures |
65 \listoffigures |
72 \clearfirst |
66 \clearfirst |
73 |
67 |
74 %\input{intro.tex} |
68 \input{Thy/document/Prelim.tex} |
75 \input{Thy/document/prelim.tex} |
69 \input{Thy/document/Logic.tex} |
76 \input{Thy/document/logic.tex} |
70 \input{Thy/document/Tactic.tex} |
77 \input{Thy/document/tactic.tex} |
71 \input{Thy/document/Proof.tex} |
78 \input{Thy/document/proof.tex} |
72 \input{Thy/document/Syntax.tex} |
79 \input{Thy/document/isar.tex} |
73 \input{Thy/document/Isar.tex} |
80 \input{Thy/document/locale.tex} |
74 \input{Thy/document/Local_Theory.tex} |
81 \input{Thy/document/integration.tex} |
75 \input{Thy/document/Integration.tex} |
82 |
76 |
83 \appendix |
77 \appendix |
84 \input{Thy/document/ML.tex} |
78 \input{Thy/document/ML.tex} |
85 |
79 |
86 \begingroup |
80 \begingroup |
87 \tocentry{\bibname} |
81 \tocentry{\bibname} |
88 \bibliographystyle{plain} \small\raggedright\frenchspacing |
82 \bibliographystyle{abbrv} \small\raggedright\frenchspacing |
89 \bibliography{../manual} |
83 \bibliography{../manual} |
90 \endgroup |
84 \endgroup |
91 |
|
92 %FIXME |
|
93 %\tocentry{\glossaryname} |
|
94 %\printglossary |
|
95 |
85 |
96 \tocentry{\indexname} |
86 \tocentry{\indexname} |
97 \printindex |
87 \printindex |
98 |
88 |
99 \end{document} |
89 \end{document} |