author | haftmann |
Sat, 05 Apr 2014 11:37:00 +0200 | |
changeset 56420 | b266e7a86485 |
parent 49003 | src/Doc/LaTeXsugar/document/root.tex@09a9761cf5ae |
child 63414 | beb987127d0f |
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 |
|
40729 | 4 |
\usepackage{amssymb} |
15337 | 5 |
|
6 |
\usepackage{mathpartir} |
|
7 |
||
8 |
% this should be the last package used |
|
48949
a773af3e37d6
more standard document preparation within session context;
wenzelm
parents:
42511
diff
changeset
|
9 |
\usepackage{pdfsetup} |
15337 | 10 |
|
11 |
% urls in roman style, theory text in math-similar italics |
|
12 |
\urlstyle{rm} |
|
13 |
\isabellestyle{it} |
|
14 |
||
15342 | 15 |
\hyphenation{Isa-belle} |
15337 | 16 |
\begin{document} |
17 |
||
33323 | 18 |
\title{\LaTeX\ Sugar for Isabelle Documents} |
15953 | 19 |
\author{Florian Haftmann, Gerwin Klein, Tobias Nipkow, Norbert Schirmer} |
15337 | 20 |
\maketitle |
21 |
||
22 |
\begin{abstract} |
|
15689 | 23 |
This document shows how to typset mathematics in Isabelle-based |
15337 | 24 |
documents in a style close to that in ordinary computer science papers. |
25 |
\end{abstract} |
|
26 |
||
16075 | 27 |
%\tableofcontents |
15337 | 28 |
|
29 |
% generated text of all theories |
|
15342 | 30 |
\input{Sugar.tex} |
15337 | 31 |
|
32 |
% optional bibliography |
|
15342 | 33 |
\bibliographystyle{abbrv} |
34 |
\bibliography{root} |
|
15337 | 35 |
|
36 |
\end{document} |
|
37 |
||
38 |
%%% Local Variables: |
|
39 |
%%% mode: latex |
|
40 |
%%% TeX-master: t |
|
41 |
%%% End: |