doc-src/LaTeXsugar/Sugar/document/root.tex
changeset 48949 a773af3e37d6
parent 48948 fa49f8890ef3
child 48950 9965099f51ad
--- a/doc-src/LaTeXsugar/Sugar/document/root.tex	Mon Aug 27 22:14:17 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-\documentclass[11pt,a4paper]{article}
-\usepackage{../../../../lib/texinputs/isabelle,../../../../lib/texinputs/isabellesym}
-
-% further packages required for unusual symbols (see also isabellesym.sty)
-% use only when needed
-\usepackage{amssymb}
-
-\usepackage{mathpartir}
-
-% this should be the last package used
-\usepackage{../../../pdfsetup}
-
-% urls in roman style, theory text in math-similar italics
-\urlstyle{rm}
-\isabellestyle{it}
-
-\hyphenation{Isa-belle}
-\begin{document}
-
-\title{\LaTeX\ Sugar for Isabelle Documents}
-\author{Florian Haftmann, Gerwin Klein, Tobias Nipkow, Norbert Schirmer}
-\maketitle
-
-\begin{abstract}
-This document shows how to typset mathematics in Isabelle-based
-documents in a style close to that in ordinary computer science papers.
-\end{abstract}
-
-%\tableofcontents
-
-% generated text of all theories
-\input{Sugar.tex}
-
-% optional bibliography
-\bibliographystyle{abbrv}
-\bibliography{root}
-
-\end{document}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: t
-%%% End: