doc-src/TutorialI/basics.tex
 changeset 9541 d17c0b34d5c8 parent 8771 026f37a86ea7 child 9689 751fde5307e4
--- 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}.