--- a/doc-src/Logics/intro.tex Fri May 16 15:54:04 1997 +0200
+++ b/doc-src/Logics/intro.tex Fri May 16 15:55:02 1997 +0200
@@ -44,13 +44,16 @@
The logics {\tt CCL}, {\tt LCF}, {\tt HOLCF}, {\tt Modal} and {\tt
Cube} are currently undocumented. All object-logics' sources are
distributed with Isabelle (see the directory \texttt{src}). They are
-also available for browsing on the WWW at
-\texttt{http://www4.informatik.tu-muenchen.de/\~\relax
- nipkow/isabelle/}.
+also available for browsing on the WWW at:
+\begin{ttbox}
+http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
+\end{ttbox}
+Note that this is not necessarily consistent with your local sources!
-You should not read this manual before reading {\em Introduction to
- Isabelle\/} and performing some Isabelle proofs. Consult the {\em
- Reference Manual} for more information on tactics, packages, etc.
+\medskip You should not read this manual before reading {\em
+ Introduction to Isabelle\/} and performing some Isabelle proofs.
+Consult the {\em Reference Manual} for more information on tactics,
+packages, etc.
\section{Syntax definitions}