--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Tue Dec 07 11:31:14 2004 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Tue Dec 07 12:13:17 2004 +0100
@@ -32,10 +32,12 @@
This document shows you how to make Isabelle and \LaTeX\ cooperate to
produce ordinary looking mathematics that hides the fact that it was
typeset by a machine. You merely need to import theory
-\texttt{LaTeXsugar} in the header of your own theory and copy the bits of
-\texttt{OptionalSugar} that you want to use. You may also
-need additional \LaTeX\ packages. These should be included
-at the beginning of your \LaTeX\ document, typically in \texttt{root.tex}.
+\texttt{LaTeXsugar} in the header of your own theory and copy the bits
+of \texttt{OptionalSugar} that you want to use. You may also need
+additional \LaTeX\ packages. These should be included at the beginning
+of your \LaTeX\ document, typically in \texttt{root.tex}.
+
+The theories and support files are available from \cite{tar}.
*}
section{* HOL syntax*}
--- a/doc-src/LaTeXsugar/Sugar/document/root.bib Tue Dec 07 11:31:14 2004 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/root.bib Tue Dec 07 12:13:17 2004 +0100
@@ -4,4 +4,9 @@
note={\url{http://www.in.tum.de/~nipkow/LNCS2283/}}}
@misc{mathpartir,author={Didier R\'emy},title={mathpartir},
-note={\url{http://cristal.inria.fr/~remy/latex/}}}
\ No newline at end of file
+note={\url{http://cristal.inria.fr/~remy/latex/}}}
+
+@misc{tar,author={Gerwin Klein and Norber Schirmer and Tobias Nipkow},
+title={{LaTeX} sugar theories and support files},
+note={\url{http://isabelle.in.tum.de/sugar.tar.gz}}}
+