# HG changeset patch
# User wenzelm
# Date 1212434028 -7200
# Node ID 220fb39be5433b3fa68655a80c97a2058adbd1b2
# Parent  d038a2ba87f64b4a4168daab01b341474f246d5f
isatool tty;

diff -r d038a2ba87f6 -r 220fb39be543 doc-src/IsarRef/Thy/Introduction.thy
--- a/doc-src/IsarRef/Thy/Introduction.thy	Mon Jun 02 21:01:42 2008 +0200
+++ b/doc-src/IsarRef/Thy/Introduction.thy	Mon Jun 02 21:13:48 2008 +0200
@@ -65,24 +65,22 @@
 subsection {* Terminal sessions *}
 
 text {*
-  Isar is already part of Isabelle.  The low-level @{verbatim
-  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:   % FIXME update
+  The Isabelle \texttt{tty} tool provides a very interface for running
+  the Isar interaction loop, with some support for command line
+  editing.  For example:
 \begin{ttbox}
-isabelle -I HOL\medskip
-\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
+isatool tty\medskip
+{\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip
 theory Foo imports Main begin;
 definition foo :: nat where "foo == 1";
 lemma "0 < foo" by (simp add: foo_def);
 end;
 \end{ttbox}
 
-  Note that any Isabelle/Isar command may be retracted by @{command
-  "undo"}.  See the Isabelle/Isar Quick Reference
-  (\appref{ap:refcard}) for a comprehensive overview of available
-  commands and other language elements.
+  Any Isabelle/Isar command may be retracted by @{command "undo"}.
+  See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a
+  comprehensive overview of available commands and other language
+  elements.
 *}
 
 
diff -r d038a2ba87f6 -r 220fb39be543 doc-src/IsarRef/Thy/document/Introduction.tex
--- a/doc-src/IsarRef/Thy/document/Introduction.tex	Mon Jun 02 21:01:42 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Introduction.tex	Mon Jun 02 21:13:48 2008 +0200
@@ -89,22 +89,22 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-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:   % FIXME update
+The Isabelle \texttt{tty} tool provides a very interface for running
+  the Isar interaction loop, with some support for command line
+  editing.  For example:
 \begin{ttbox}
-isabelle -I HOL\medskip
-\out{> Welcome to Isabelle/HOL (Isabelle2005)}\medskip
+isatool tty\medskip
+{\out Welcome to Isabelle/HOL (Isabelle2008)}\medskip
 theory Foo imports Main begin;
 definition foo :: nat where "foo == 1";
 lemma "0 < foo" by (simp add: foo_def);
 end;
 \end{ttbox}
 
-  Note that any Isabelle/Isar command may be retracted by \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}.  See the Isabelle/Isar Quick Reference
-  (\appref{ap:refcard}) for a comprehensive overview of available
-  commands and other language elements.%
+  Any Isabelle/Isar command may be retracted by \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}.
+  See the Isabelle/Isar Quick Reference (\appref{ap:refcard}) for a
+  comprehensive overview of available commands and other language
+  elements.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %