# HG changeset patch
# User wenzelm
# Date 941193914 -7200
# Node ID a15748c3b7e41dcce83c37a3d1f38817b61b4328
# Parent  7a20317850ab18363e83ba0623f7913c2f89d964
\isasym;

diff -r 7a20317850ab -r a15748c3b7e4 doc-src/System/present.tex
--- a/doc-src/System/present.tex	Fri Oct 29 10:10:31 1999 +0200
+++ b/doc-src/System/present.tex	Fri Oct 29 12:45:14 1999 +0200
@@ -282,9 +282,18 @@
 \texttt{isabelle.sty} as distributed with Isabelle.  Doing
 \verb,\usepackage{isabelle}, somewhere in \texttt{root.tex} should work fine;
 the underlying Isabelle \texttt{latex} utility already includes an appropriate
-{\TeX} inputs path.  For proper setup of PDF documents (with hyperlinks,
-bookmarks, and thumbnail images), we recommend to include \verb,pdfsetup.sty,
-as well.\footnote{It is safe to do so even without using PDF~\LaTeX.}
+{\TeX} inputs path.
+
+If the text contains any references to Isabelle symbols (such as
+\verb,\<forall>,) then \texttt{isabellesym.sty} should be included as well.
+This package contains a standard set of {\LaTeX} macro definitions
+\verb,\isasym,$foo$ corresponding to \verb,\<,$foo$\verb,>,.  The user may
+refer to further symbols as well, simply by providing {\LaTeX} macros of the
+same sort.
+
+For proper setup of PDF documents (with hyperlinks, bookmarks, and thumbnail
+images), we recommend to include \verb,pdfsetup.sty, as well.  It is safe to
+do so even without using PDF~\LaTeX.
 
 \medskip As a final step, \texttt{isatool document} is run on the resulting
 \texttt{document} directory.  Thus the actual output document is built and