src/Doc/Sugar/document/root.tex
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--
closer correspondence of document and session names, while maintaining document names for external reference
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15337
nipkow
parents:
diff changeset
     1
\documentclass[11pt,a4paper]{article}
48949
a773af3e37d6 more standard document preparation within session context;
wenzelm
parents: 42511
diff changeset
     2
\usepackage{isabelle,isabellesym}
15337
nipkow
parents:
diff changeset
     3
40729
ebb0c9657b03 eliminated some generated comments;
wenzelm
parents: 33323
diff changeset
     4
\usepackage{amssymb}
15337
nipkow
parents:
diff changeset
     5
nipkow
parents:
diff changeset
     6
\usepackage{mathpartir}
nipkow
parents:
diff changeset
     7
nipkow
parents:
diff changeset
     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
nipkow
parents:
diff changeset
    10
nipkow
parents:
diff changeset
    11
% urls in roman style, theory text in math-similar italics
nipkow
parents:
diff changeset
    12
\urlstyle{rm}
nipkow
parents:
diff changeset
    13
\isabellestyle{it}
nipkow
parents:
diff changeset
    14
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    15
\hyphenation{Isa-belle}
15337
nipkow
parents:
diff changeset
    16
\begin{document}
nipkow
parents:
diff changeset
    17
33323
1932908057c7 small fixes
nipkow
parents: 26911
diff changeset
    18
\title{\LaTeX\ Sugar for Isabelle Documents}
15953
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15689
diff changeset
    19
\author{Florian Haftmann, Gerwin Klein, Tobias Nipkow, Norbert Schirmer}
15337
nipkow
parents:
diff changeset
    20
\maketitle
nipkow
parents:
diff changeset
    21
nipkow
parents:
diff changeset
    22
\begin{abstract}
15689
621bd0d8048f section on qmark
nipkow
parents: 15493
diff changeset
    23
This document shows how to typset mathematics in Isabelle-based
15337
nipkow
parents:
diff changeset
    24
documents in a style close to that in ordinary computer science papers.
nipkow
parents:
diff changeset
    25
\end{abstract}
nipkow
parents:
diff changeset
    26
16075
8852058ecf8d added ? explanations
nipkow
parents: 15953
diff changeset
    27
%\tableofcontents
15337
nipkow
parents:
diff changeset
    28
nipkow
parents:
diff changeset
    29
% generated text of all theories
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    30
\input{Sugar.tex}
15337
nipkow
parents:
diff changeset
    31
nipkow
parents:
diff changeset
    32
% optional bibliography
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    33
\bibliographystyle{abbrv}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    34
\bibliography{root}
15337
nipkow
parents:
diff changeset
    35
nipkow
parents:
diff changeset
    36
\end{document}
nipkow
parents:
diff changeset
    37
nipkow
parents:
diff changeset
    38
%%% Local Variables:
nipkow
parents:
diff changeset
    39
%%% mode: latex
nipkow
parents:
diff changeset
    40
%%% TeX-master: t
nipkow
parents:
diff changeset
    41
%%% End: