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