equal
deleted
inserted
replaced
2 \usepackage{latexsym,graphicx} |
2 \usepackage{latexsym,graphicx} |
3 \usepackage[refpage]{nomencl} |
3 \usepackage[refpage]{nomencl} |
4 \usepackage{../iman,../extra,../isar,../proof} |
4 \usepackage{../iman,../extra,../isar,../proof} |
5 \usepackage[nohyphen,strings]{../underscore} |
5 \usepackage[nohyphen,strings]{../underscore} |
6 \usepackage{../isabelle,../isabellesym} |
6 \usepackage{../isabelle,../isabellesym} |
|
7 \usepackage{../ttbox,../rail,../railsetup} |
7 \usepackage{style} |
8 \usepackage{style} |
8 \usepackage{../pdfsetup} |
9 \usepackage{../pdfsetup} |
9 |
10 |
10 |
11 |
11 \hyphenation{Isabelle} |
12 \hyphenation{Isabelle} |
19 Florian Haftmann |
20 Florian Haftmann |
20 and Larry Paulson |
21 and Larry Paulson |
21 } |
22 } |
22 |
23 |
23 \makeindex |
24 \makeindex |
|
25 |
|
26 \railterm{lbrace,rbrace,atsign} |
|
27 \railalias{lbracesym}{\isasymlbrace}\railterm{lbracesym} |
|
28 \railalias{rbracesym}{\isasymrbrace}\railterm{rbracesym} |
|
29 \railalias{dots}{\isasymdots}\railterm{dots} |
24 |
30 |
25 |
31 |
26 \begin{document} |
32 \begin{document} |
27 |
33 |
28 \maketitle |
34 \maketitle |
74 \pagenumbering{roman} |
80 \pagenumbering{roman} |
75 \tableofcontents |
81 \tableofcontents |
76 \listoffigures |
82 \listoffigures |
77 \clearfirst |
83 \clearfirst |
78 |
84 |
|
85 \setcounter{chapter}{-1} |
|
86 |
|
87 \input{Thy/document/ML.tex} |
79 \input{Thy/document/Prelim.tex} |
88 \input{Thy/document/Prelim.tex} |
80 \input{Thy/document/Logic.tex} |
89 \input{Thy/document/Logic.tex} |
|
90 \input{Thy/document/Syntax.tex} |
81 \input{Thy/document/Tactic.tex} |
91 \input{Thy/document/Tactic.tex} |
82 \input{Thy/document/Proof.tex} |
92 \input{Thy/document/Proof.tex} |
83 \input{Thy/document/Syntax.tex} |
|
84 \input{Thy/document/Isar.tex} |
93 \input{Thy/document/Isar.tex} |
85 \input{Thy/document/Local_Theory.tex} |
94 \input{Thy/document/Local_Theory.tex} |
86 \input{Thy/document/Integration.tex} |
95 \input{Thy/document/Integration.tex} |
87 |
|
88 \appendix |
|
89 \input{Thy/document/ML.tex} |
|
90 |
96 |
91 \begingroup |
97 \begingroup |
92 \tocentry{\bibname} |
98 \tocentry{\bibname} |
93 \bibliographystyle{abbrv} \small\raggedright\frenchspacing |
99 \bibliographystyle{abbrv} \small\raggedright\frenchspacing |
94 \bibliography{../manual} |
100 \bibliography{../manual} |