equal
deleted
inserted
replaced
|
1 \documentclass[11pt,a4paper]{article} |
|
2 \usepackage{isabelle,isabellesym} |
|
3 |
|
4 % further packages required for unusual symbols (see also isabellesym.sty) |
|
5 % use only when needed |
|
6 \usepackage{amssymb} |
|
7 |
|
8 \usepackage{mathpartir} |
|
9 |
|
10 % this should be the last package used |
|
11 \usepackage{pdfsetup} |
|
12 |
|
13 % urls in roman style, theory text in math-similar italics |
|
14 \urlstyle{rm} |
|
15 \isabellestyle{it} |
|
16 |
|
17 \hyphenation{Isa-belle} |
|
18 \begin{document} |
|
19 |
|
20 \title{\LaTeX\ Sugar for Isabelle Documents} |
|
21 \author{Florian Haftmann, Gerwin Klein, Tobias Nipkow, Norbert Schirmer} |
|
22 \maketitle |
|
23 |
|
24 \begin{abstract} |
|
25 This document shows how to typset mathematics in Isabelle-based |
|
26 documents in a style close to that in ordinary computer science papers. |
|
27 \end{abstract} |
|
28 |
|
29 %\tableofcontents |
|
30 |
|
31 % generated text of all theories |
|
32 \input{Sugar.tex} |
|
33 |
|
34 % optional bibliography |
|
35 \bibliographystyle{abbrv} |
|
36 \bibliography{root} |
|
37 |
|
38 \end{document} |
|
39 |
|
40 %%% Local Variables: |
|
41 %%% mode: latex |
|
42 %%% TeX-master: t |
|
43 %%% End: |