1.1 --- a/doc-src/IsarRef/Thy/Introduction.thy	Mon Jun 02 21:01:42 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Introduction.thy	Mon Jun 02 21:13:48 2008 +0200
     1.3 @@ -65,24 +65,22 @@
     1.4  subsection {* Terminal sessions *}
     1.5  
     1.6  text {*
     1.7 -  Isar is already part of Isabelle.  The low-level @{verbatim
     1.8 -  isabelle} binary provides option @{verbatim "-I"} to run the
     1.9 -  Isabelle/Isar interaction loop at startup, rather than the raw ML
    1.10 -  top-level.  So the most basic way to do anything with Isabelle/Isar
    1.11 -  is as follows:   % FIXME update
    1.12 +  The Isabelle \texttt{tty} tool provides a very interface for running
    1.13 +  the Isar interaction loop, with some support for command line
    1.14 +  editing.  For example:
    1.15  \begin{ttbox}
    1.16 -isabelle -I HOL\medskip
    1.17 -\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
    1.18 +isatool tty\medskip
    1.19 +{\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip
    1.20  theory Foo imports Main begin;
    1.21  definition foo :: nat where "foo == 1";
    1.22  lemma "0 < foo" by (simp add: foo_def);
    1.23  end;
    1.24  \end{ttbox}
    1.25  
    1.26 -  Note that any Isabelle/Isar command may be retracted by @{command
    1.27 -  "undo"}.  See the Isabelle/Isar Quick Reference
    1.28 -  (\appref{ap:refcard}) for a comprehensive overview of available
    1.29 -  commands and other language elements.
    1.30 +  Any Isabelle/Isar command may be retracted by @{command "undo"}.
    1.31 +  See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a
    1.32 +  comprehensive overview of available commands and other language
    1.33 +  elements.
    1.34  *}
    1.35  
    1.36