--- a/doc-src/IsarRef/Thy/document/intro.tex Thu May 15 20:02:42 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/intro.tex Thu May 15 20:02:44 2008 +0200
@@ -250,13 +250,10 @@
\begin{isamarkuptext}%
Isabelle/Isar provides a simple document preparation system based on
existing {PDF-\LaTeX} technology, with full support of hyper-links
- (both local references and URLs), bookmarks, and thumbnails. Thus
- the results are equally well suited for WWW browsing and as printed
- copies.
+ (both local references and URLs) and bookmarks. Thus the results
+ are equally well suited for WWW browsing and as printed copies.
- \medskip
-
- Isabelle generates {\LaTeX} output as part of the run of a
+ \medskip Isabelle generates {\LaTeX} output as part of the run of a
\emph{logic session} (see also \cite{isabelle-sys}). Getting
started with a working configuration for common situations is quite
easy by using the Isabelle \verb|mkdir| and \verb|make|