| author | wenzelm |
| Wed, 01 Jun 2016 16:02:02 +0200 | |
| changeset 63209 | 82cd1d481eb9 |
| parent 56420 | b266e7a86485 |
| 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: |