# HG changeset patch
# User wenzelm
# Date 915631212 -3600
# Node ID 0f8ab32093ae088c0e29a7b2bcb8d3660606f492
# Parent  f4f0d637747c3fd57c7f0fea32e605ed9bae2d78
fixed commit spec;

diff -r f4f0d637747c -r 0f8ab32093ae doc-src/Ref/introduction.tex
--- a/doc-src/Ref/introduction.tex	Wed Jan 06 14:21:44 1999 +0100
+++ b/doc-src/Ref/introduction.tex	Wed Jan 06 15:00:12 1999 +0100
@@ -94,7 +94,7 @@
 \begin{ttbox} 
 quit    : unit -> unit
 exit    : int -> unit
-commit  : unit -> unit
+commit  : unit -> bool
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{quit}();] ends the Isabelle session, without saving
@@ -104,7 +104,8 @@
   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.
+  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