doc-src/Ref/introduction.tex

tuned comment

\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: