doc-src/Ref/introduction.tex
changeset 3200 ea2310ba01da
parent 3108 335efc3f5632
child 3485 f27a30a18a17
     1.1 --- a/doc-src/Ref/introduction.tex	Thu May 15 14:49:41 1997 +0200
     1.2 +++ b/doc-src/Ref/introduction.tex	Thu May 15 14:58:51 1997 +0200
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  %% $Id$
     1.6  
     1.7  \chapter{Basic Use of Isabelle}\index{sessions|(} 
     1.8 @@ -71,9 +72,8 @@
     1.9  isabelle Foo  
    1.10  \end{ttbox}
    1.11  
    1.12 -%FIXME not yet
    1.13 -%More details about \texttt{isabelle} may be found in the \emph{System
    1.14 -%  Manual}.
    1.15 +More details about \texttt{isabelle} may be found in the \emph{System
    1.16 +  Manual}.
    1.17  
    1.18  \medskip Saving the state is not enough.  Record, on a file, the
    1.19  top-level commands that generate your theories and proofs.  Such a
    1.20 @@ -89,9 +89,8 @@
    1.21  are a number of external utilities available. These are started
    1.22  uniformly via the \texttt{isatool} wrapper.
    1.23  
    1.24 -%FIXME not yet
    1.25 -%Again, see the \emph{System Manual} for more information user
    1.26 -%interfaces and utilities.
    1.27 +Again, see the \emph{System Manual} for more information user
    1.28 +interfaces and utilities.
    1.29  
    1.30  
    1.31  \section{Ending a session}
    1.32 @@ -270,36 +269,4 @@
    1.33    theory used in the last interactive proof.
    1.34  \end{warn}
    1.35  
    1.36 -%FIXME remove
    1.37 -%\section{Shell scripts}\label{sec:shell-scripts}
    1.38 -%\index{shell scripts|bold} The following files are distributed with
    1.39 -%Isabelle, and work under Unix$^{\rm TM}$.  They can be executed as commands
    1.40 -%to the Unix shell.  Some of them depend upon shell environment variables.
    1.41 -%\begin{ttdescription}
    1.42 -%\item[make-all $switches$] \index{*make-all shell script}
    1.43 -%  compiles the Isabelle system, when executed on the source directory.
    1.44 -%  Environment variables specify which \ML{} compiler to use.  These
    1.45 -%  variables, and the {\it switches}, are documented on the file itself.
    1.46 -%
    1.47 -%\item[teeinput $program$] \index{*teeinput shell script}
    1.48 -%  executes the {\it program}, while piping the standard input to a log file
    1.49 -%  designated by the \verb|$LISTEN| environment variable.  Normally the
    1.50 -%  program is Isabelle, and the log file receives a copy of all the Isabelle
    1.51 -%  commands.
    1.52 -%
    1.53 -%\item[xlisten $program$] \index{*xlisten shell script}
    1.54 -%  is a trivial `user interface' for the X Window System.  It creates two
    1.55 -%  windows using {\tt xterm}.  One executes an interactive session via
    1.56 -%  \hbox{\tt teeinput $program$}, while the other displays the log file.  To
    1.57 -%  make a proof record, simply paste lines from the log file into an editor
    1.58 -%  window.
    1.59 -%
    1.60 -%\item[expandshort $files$]  \index{*expandshort shell script}
    1.61 -%  reads the {\it files\/} and replaces all occurrences of the shorthand
    1.62 -%  commands {\tt br}, {\tt be}, {\tt brs}, {\tt bes}, etc., with the
    1.63 -%  corresponding full commands.  Shorthand commands should appear one
    1.64 -%  per line.  The old versions of the files
    1.65 -%  are renamed to have the suffix~\verb'~~'.
    1.66 -%\end{ttdescription}
    1.67 -
    1.68  \index{sessions|)}