Added instructions on starting up
Tue, 26 Nov 1996 16:07:17 +0100
changeset 2225 78a8faae780f
parent 2224 4fc4b465be5b
child 2226 f3c6a22681b1
Added instructions on starting up
--- a/doc-src/Ref/introduction.tex	Tue Nov 26 15:59:28 1996 +0100
+++ b/doc-src/Ref/introduction.tex	Tue Nov 26 16:07:17 1996 +0100
@@ -17,6 +17,22 @@
 \section{Basic interaction with Isabelle}
+\index{starting up|bold}\nobreak
+First, read the instructions on file {\tt README} in the top-level
+distribution directory.  Follow them to create the object-logics you need
+on a directory you have created to hold binary images.  Suppose the
+environment variable {\tt ISABELLEBIN} refers to this directory.  The
+instructions for starting up a logic (say {\tt HOL}) depend upon which
+Standard ML compiler you are using.
+\item With Standard ML of New Jersey, type \verb|$ISABELLEBIN/HOL|.
+\item With Poly/ML, type \verb|poly $ISABELLEBIN/HOL|, possibly prefixing the
+  command with the directory where {\tt poly} is kept.
+Either way, you will find yourself at the \ML{} top level.  All Isabelle
+commands are bound to \ML{} identifiers.
 \index{saving your work|bold}
 Isabelle provides no means of storing theorems or proofs on files.
 Theorems are simply part of the \ML{} state and are named by \ML{}