# HG changeset patch
# User wenzelm
# Date 966271549 -7200
# Node ID abe51fcb222205b178382be8cb792b6069a2031e
# Parent  816917b6c2de301f6179664f7aa4fb3fb405bf95
tuned;

diff -r 816917b6c2de -r abe51fcb2222 doc-src/IsarRef/intro.tex
--- a/doc-src/IsarRef/intro.tex	Mon Aug 14 18:45:31 2000 +0200
+++ b/doc-src/IsarRef/intro.tex	Mon Aug 14 18:45:49 2000 +0200
@@ -6,9 +6,9 @@
 \subsection{Terminal sessions}
 
 Isar is already part of Isabelle (as of version Isabelle99, or later).  The
-\texttt{isabelle} binary provides option \texttt{-I} to run the Isar
-interaction loop at startup, rather than the plain ML top-level.  Thus the
-quickest way to do \emph{anything} with Isabelle/Isar is as follows:
+\texttt{isabelle} binary provides option \texttt{-I} to run the Isabelle/Isar
+interaction loop at startup, rather than the raw ML top-level.  So the
+quickest way to do anything with Isabelle/Isar is as follows:
 \begin{ttbox}
 isabelle -I HOL\medskip
 \out{> Welcome to Isabelle/HOL (Isabelle99-1)}\medskip
@@ -101,11 +101,10 @@
 Using proper mathematical symbols in Isabelle theories can be very convenient
 for readability of large formulas.  On the other hand, the plain ASCII sources
 easily become somewhat unintelligible.  For example, $\forall$ will appear as
-\verb,\\<forall>, according the default set of Isabelle symbols.
-Nevertheless, the Isabelle document preparation system (see
-\S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly.
-It is even possible to invent additional notation beyond the display
-capabilities of XEmacs and X-Symbol.
+\verb,\<forall>, according the default set of Isabelle symbols.  Nevertheless,
+the Isabelle document preparation system (see \S\ref{sec:document-prep}) will
+be happy to print non-ASCII symbols properly.  It is even possible to invent
+additional notation beyond the display capabilities of XEmacs and X-Symbol.
 
 
 \section{Isabelle/Isar theories}