equal
deleted
inserted
replaced
1 |
|
2 %% $Id$ |
|
3 |
1 |
4 \documentclass[12pt,a4paper,fleqn]{report} |
2 \documentclass[12pt,a4paper,fleqn]{report} |
5 \usepackage{latexsym,graphicx} |
3 \usepackage{latexsym,graphicx} |
6 \usepackage[refpage]{nomencl} |
4 \usepackage[refpage]{nomencl} |
7 \usepackage{../../iman,../../extra,../../isar,../../proof} |
5 \usepackage{../../iman,../../extra,../../isar,../../proof} |
10 \usepackage{pgf} |
8 \usepackage{pgf} |
11 \usepackage{pgflibraryshapes} |
9 \usepackage{pgflibraryshapes} |
12 \usepackage{tikz} |
10 \usepackage{tikz} |
13 \usepackage{../../pdfsetup} |
11 \usepackage{../../pdfsetup} |
14 |
12 |
15 %% setup |
|
16 |
|
17 % hyphenation |
|
18 \hyphenation{Isabelle} |
13 \hyphenation{Isabelle} |
19 \hyphenation{Isar} |
14 \hyphenation{Isar} |
20 |
|
21 % logical markup |
|
22 \newcommand{\strong}[1]{{\bfseries {#1}}} |
|
23 \newcommand{\qn}[1]{\emph{#1}} |
|
24 |
|
25 % typographic conventions |
|
26 \newcommand{\qt}[1]{``{#1}''} |
|
27 |
|
28 % verbatim text |
|
29 \newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}} |
|
30 |
|
31 % invisibility |
|
32 \isadroptag{theory} |
15 \isadroptag{theory} |
33 |
|
34 % quoted segments |
|
35 \makeatletter |
|
36 \isakeeptag{quote} |
|
37 \newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}} |
|
38 \renewcommand{\isatagquote}{\begin{quotesegment}} |
|
39 \renewcommand{\endisatagquote}{\end{quotesegment}} |
|
40 \makeatother |
|
41 |
|
42 \isakeeptag{quotett} |
|
43 \renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle} |
|
44 \renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle} |
|
45 |
|
46 % hack |
|
47 \newcommand{\isasymSML}{SML} |
|
48 |
|
49 |
|
50 %% contents |
|
51 |
16 |
52 \title{\includegraphics[scale=0.5]{isabelle_isar} |
17 \title{\includegraphics[scale=0.5]{isabelle_isar} |
53 \\[4ex] Code generation from Isabelle/HOL theories} |
18 \\[4ex] Code generation from Isabelle/HOL theories} |
54 \author{\emph{Florian Haftmann}} |
19 \author{\emph{Florian Haftmann}} |
55 |
20 |
73 \input{Thy/document/Adaption.tex} |
38 \input{Thy/document/Adaption.tex} |
74 \input{Thy/document/Further.tex} |
39 \input{Thy/document/Further.tex} |
75 \input{Thy/document/ML.tex} |
40 \input{Thy/document/ML.tex} |
76 |
41 |
77 \begingroup |
42 \begingroup |
78 %\tocentry{\bibname} |
|
79 \bibliographystyle{plain} \small\raggedright\frenchspacing |
43 \bibliographystyle{plain} \small\raggedright\frenchspacing |
80 \bibliography{../../manual} |
44 \bibliography{../../manual} |
81 \endgroup |
45 \endgroup |
82 |
46 |
83 \end{document} |
47 \end{document} |