diff -r 0736fa14c275 -r 978cefd606ad doc-src/IsarRef/Thy/document/intro.tex
--- a/doc-src/IsarRef/Thy/document/intro.tex	Sat May 24 22:04:46 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/intro.tex	Sat May 24 22:04:48 2008 +0200
@@ -92,8 +92,8 @@
 Isar is already part of Isabelle.  The low-level \verb|isabelle| binary provides option \verb|-I| to run the
   Isabelle/Isar interaction loop at startup, rather than the raw ML
   top-level.  So the most basic way to do anything with Isabelle/Isar
-  is as follows:
-\begin{ttbox}  % FIXME update
+  is as follows:   % FIXME update
+\begin{ttbox}
 isabelle -I HOL\medskip
 \out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
 theory Foo imports Main begin;