doc-src/LaTeXsugar/Sugar/generated/root.tex
changeset 15894 41f9c0902db1
parent 15893 c0cd613a49eb
child 15895 6bd7d0a04252
--- a/doc-src/LaTeXsugar/Sugar/generated/root.tex	Sat Apr 30 02:43:45 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-\documentclass[11pt,a4paper]{article}
-\usepackage{isabelle,isabellesym}
-
-% further packages required for unusual symbols (see also isabellesym.sty)
-% use only when needed
-%\usepackage{amssymb}                  % for \<leadsto>, \<box>, \<diamond>,
-                                       % \<sqsupset>, \<mho>, \<Join>, 
-                                       % \<lhd>, \<lesssim>, \<greatersim>,
-                                       % \<lessapprox>, \<greaterapprox>,
-                                       % \<triangleq>, \<yen>, \<lozenge>
-%\usepackage[greek,english]{babel}     % greek for \<euro>,
-                                       % english for \<guillemotleft>, 
-                                       %             \<guillemotright>
-                                       % default language = last
-%\usepackage[latin1]{inputenc}         % for \<onesuperior>, \<onequarter>,
-                                       % \<twosuperior>, \<onehalf>,
-                                       % \<threesuperior>, \<threequarters>,
-                                       % \<degree>
-%\usepackage[only,bigsqcap]{stmaryrd}  % for \<Sqinter>
-%\usepackage{eufrak}                   % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
-                                       % (only needed if amssymb not used)
-%\usepackage{textcomp}                 % for \<cent>, \<currency>
-
-\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{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: