reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
\chapter{Basic Use of Isabelle}
\section{Ending a session}
\begin{ttbox}
quit : unit -> unit
exit : int -> unit
commit : unit -> bool
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{quit}();] ends the Isabelle session, without saving
the state.
\item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return
code \(i\) to the operating system.
\item[\ttindexbold{commit}();] saves the current state without ending
the session, provided that the logic image is opened read-write;
return value {\tt false} indicates an error.
\end{ttdescription}
Typing control-D also finishes the session in essentially the same way
as the sequence {\tt commit(); quit();} would.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "ref"
%%% End: