diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Fri Aug 04 23:02:11 2000 +0200
+++ b/doc-src/TutorialI/basics.tex	Sun Aug 06 15:26:53 2000 +0200
@@ -65,7 +65,11 @@
 \begin{center}\small
     \url{http://isabelle.in.tum.de/library/}
 \end{center}
-and is recommended browsing.
+and is recommended browsing. Note that most of the theories in the library
+are based on classical Isabelle without the Isar extension. This means that
+they look slightly different than the theories in this tutorial, and that all
+proofs are in separate ML files.
+
 \begin{warn}
   HOL contains a theory \ttindexbold{Main}, the union of all the basic
   predefined theories like arithmetic, lists, sets, etc.\ (see the online
@@ -275,13 +279,11 @@
 mathematical symbols. For those that do not, remember that ASCII-equivalents
 are shown in figure~\ref{fig:ascii} in the appendix.
 
-Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces,
-for example Proof General, require each command to be terminated by a
-semicolon, whereas others, for example the shell level, do not. But even at
-the shell level it is advisable to use semicolons to enforce that a command
+Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} 
+Commands may but need not be terminated by semicolons.
+At the shell level it is advisable to use semicolons to enforce that a command
 is executed immediately; otherwise Isabelle may wait for the next keyword
-before it knows that the command is complete. Note that for readibility
-reasons we often drop the final semicolon in the text.
+before it knows that the command is complete.
 
 
 \section{Getting started}
@@ -296,3 +298,4 @@
 type each command into the file first and then enter it into Isabelle by
 copy-and-paste, thus ensuring that you have a complete record of your theory.
 As mentioned above, Proof General offers a much superior interface.
+If you have installed Proof General, you can start it with \texttt{Isabelle}.