# HG changeset patch
# User wenzelm
# Date 1211659486 -7200
# Node ID 0736fa14c275886474fdcf98854bc8c1c15ea95f
# Parent  51c5acd57b756ac22badcc74badbac484e020356
invisible comment;

diff -r 51c5acd57b75 -r 0736fa14c275 doc-src/IsarRef/Thy/intro.thy
--- 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;