# HG changeset patch
# User kleing
# Date 1102417997 -3600
# Node ID b1c5add0a65e411c7b237e2b223f5b297f9d05f9
# Parent  3d99eea28a9bee062c9c74ddeba93497be9b6897
link to tar.gz

diff -r 3d99eea28a9b -r b1c5add0a65e doc-src/LaTeXsugar/Sugar/Sugar.thy
--- 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*}
diff -r 3d99eea28a9b -r b1c5add0a65e doc-src/LaTeXsugar/Sugar/document/root.bib
--- 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}}}
+