Fri, 29 Oct 1999 12:45:14 +0200
changeset 7970 a15748c3b7e4
parent 7969 7a20317850ab
child 7971 023778c8a029
--- 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