69 by running |
70 by running |
70 \begin{ttbox} |
71 \begin{ttbox} |
71 isabelle Foo |
72 isabelle Foo |
72 \end{ttbox} |
73 \end{ttbox} |
73 |
74 |
74 %FIXME not yet |
75 More details about \texttt{isabelle} may be found in the \emph{System |
75 %More details about \texttt{isabelle} may be found in the \emph{System |
76 Manual}. |
76 % Manual}. |
|
77 |
77 |
78 \medskip Saving the state is not enough. Record, on a file, the |
78 \medskip Saving the state is not enough. Record, on a file, the |
79 top-level commands that generate your theories and proofs. Such a |
79 top-level commands that generate your theories and proofs. Such a |
80 record allows you to replay the proofs whenever required, for instance |
80 record allows you to replay the proofs whenever required, for instance |
81 after making minor changes to the axioms. Ideally, your record will |
81 after making minor changes to the axioms. Ideally, your record will |
87 \texttt{Isabelle} executable (note the capital I) runs one such |
87 \texttt{Isabelle} executable (note the capital I) runs one such |
88 interface, depending on your local configuration. Furthermore there |
88 interface, depending on your local configuration. Furthermore there |
89 are a number of external utilities available. These are started |
89 are a number of external utilities available. These are started |
90 uniformly via the \texttt{isatool} wrapper. |
90 uniformly via the \texttt{isatool} wrapper. |
91 |
91 |
92 %FIXME not yet |
92 Again, see the \emph{System Manual} for more information user |
93 %Again, see the \emph{System Manual} for more information user |
93 interfaces and utilities. |
94 %interfaces and utilities. |
|
95 |
94 |
96 |
95 |
97 \section{Ending a session} |
96 \section{Ending a session} |
98 \begin{ttbox} |
97 \begin{ttbox} |
99 quit : unit -> unit |
98 quit : unit -> unit |
268 pretty printing information from the proof state last stored in the |
267 pretty printing information from the proof state last stored in the |
269 subgoal module. The appearance of the output thus depends upon the |
268 subgoal module. The appearance of the output thus depends upon the |
270 theory used in the last interactive proof. |
269 theory used in the last interactive proof. |
271 \end{warn} |
270 \end{warn} |
272 |
271 |
273 %FIXME remove |
|
274 %\section{Shell scripts}\label{sec:shell-scripts} |
|
275 %\index{shell scripts|bold} The following files are distributed with |
|
276 %Isabelle, and work under Unix$^{\rm TM}$. They can be executed as commands |
|
277 %to the Unix shell. Some of them depend upon shell environment variables. |
|
278 %\begin{ttdescription} |
|
279 %\item[make-all $switches$] \index{*make-all shell script} |
|
280 % compiles the Isabelle system, when executed on the source directory. |
|
281 % Environment variables specify which \ML{} compiler to use. These |
|
282 % variables, and the {\it switches}, are documented on the file itself. |
|
283 % |
|
284 %\item[teeinput $program$] \index{*teeinput shell script} |
|
285 % executes the {\it program}, while piping the standard input to a log file |
|
286 % designated by the \verb|$LISTEN| environment variable. Normally the |
|
287 % program is Isabelle, and the log file receives a copy of all the Isabelle |
|
288 % commands. |
|
289 % |
|
290 %\item[xlisten $program$] \index{*xlisten shell script} |
|
291 % is a trivial `user interface' for the X Window System. It creates two |
|
292 % windows using {\tt xterm}. One executes an interactive session via |
|
293 % \hbox{\tt teeinput $program$}, while the other displays the log file. To |
|
294 % make a proof record, simply paste lines from the log file into an editor |
|
295 % window. |
|
296 % |
|
297 %\item[expandshort $files$] \index{*expandshort shell script} |
|
298 % reads the {\it files\/} and replaces all occurrences of the shorthand |
|
299 % commands {\tt br}, {\tt be}, {\tt brs}, {\tt bes}, etc., with the |
|
300 % corresponding full commands. Shorthand commands should appear one |
|
301 % per line. The old versions of the files |
|
302 % are renamed to have the suffix~\verb'~~'. |
|
303 %\end{ttdescription} |
|
304 |
|
305 \index{sessions|)} |
272 \index{sessions|)} |