# HG changeset patch
# User paulson
# Date 849020837 -3600
# Node ID 78a8faae780ff037ed7e5cb082e74d916cd1c93d
# Parent  4fc4b465be5b93e11687acc64826b3f03fe65ae3
Added instructions on starting up

diff -r 4fc4b465be5b -r 78a8faae780f doc-src/Ref/introduction.tex
--- 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.
+\begin{itemize}
+\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.
+\end{itemize}
+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{}