--- a/doc-src/IsarRef/Thy/intro.thy Sat May 24 22:04:44 2008 +0200
+++ b/doc-src/IsarRef/Thy/intro.thy Sat May 24 22:04:46 2008 +0200
@@ -69,8 +69,8 @@
isabelle} binary provides option @{verbatim "-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;