--- 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}.