--- 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%
%