author | wenzelm |
Mon, 27 Aug 2012 22:22:42 +0200 | |
changeset 48949 | a773af3e37d6 |
parent 42511 | doc-src/LaTeXsugar/Sugar/document/root.tex@bf89455ccf9d |
permissions | -rw-r--r-- |
15337 | 1 |
\documentclass[11pt,a4paper]{article} |
48949
a773af3e37d6
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
2 |
\usepackage{isabelle,isabellesym} |
15337 | 3 |
|
4 |
% further packages required for unusual symbols (see also isabellesym.sty) |
|
5 |
% use only when needed |
|
40729 | 6 |
\usepackage{amssymb} |
15337 | 7 |
|
8 |
\usepackage{mathpartir} |
|
9 |
||
10 |
% this should be the last package used |
|
48949
a773af3e37d6
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
11 |
\usepackage{pdfsetup} |
15337 | 12 |
|
13 |
% urls in roman style, theory text in math-similar italics |
|
14 |
\urlstyle{rm} |
|
15 |
\isabellestyle{it} |
|
16 |
||
15342 | 17 |
\hyphenation{Isa-belle} |
15337 | 18 |
\begin{document} |
19 |
||
33323 | 20 |
\title{\LaTeX\ Sugar for Isabelle Documents} |
15953 | 21 |
\author{Florian Haftmann, Gerwin Klein, Tobias Nipkow, Norbert Schirmer} |
15337 | 22 |
\maketitle |
23 |
||
24 |
\begin{abstract} |
|
15689 | 25 |
This document shows how to typset mathematics in Isabelle-based |
15337 | 26 |
documents in a style close to that in ordinary computer science papers. |
27 |
\end{abstract} |
|
28 |
||
16075 | 29 |
%\tableofcontents |
15337 | 30 |
|
31 |
% generated text of all theories |
|
15342 | 32 |
\input{Sugar.tex} |
15337 | 33 |
|
34 |
% optional bibliography |
|
15342 | 35 |
\bibliographystyle{abbrv} |
36 |
\bibliography{root} |
|
15337 | 37 |
|
38 |
\end{document} |
|
39 |
||
40 |
%%% Local Variables: |
|
41 |
%%% mode: latex |
|
42 |
%%% TeX-master: t |
|
43 |
%%% End: |