changeset 6148 d97a944c6ea3
parent 5375 1463e182c533
child 6584 5569f2672662
--- a/doc-src/Tutorial/basics.tex	Wed Jan 20 17:59:19 1999 +0100
+++ b/doc-src/Tutorial/basics.tex	Wed Jan 20 18:07:34 1999 +0100
@@ -42,8 +42,12 @@
 Everything defined in the parent theories (and their parents \dots) is
 automatically visible. To avoid name clashes, identifiers can be qualified by
 theory names as in \texttt{T.f} and \texttt{B.f}. HOL's theory library is
-available online at \verb$$ and is
-recommended browsing.
+available online at
+and is recommended browsing.
   HOL contains a theory \ttindexbold{Main}, the union of all the basic
   predefined theories like arithmetic, lists, sets, etc.\ (see the online