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