equal
deleted
inserted
replaced
1 |
|
2 \chapter{Basic Use of Isabelle} |
|
3 |
|
4 \section{Ending a session} |
|
5 \begin{ttbox} |
|
6 quit : unit -> unit |
|
7 exit : int -> unit |
|
8 commit : unit -> bool |
|
9 \end{ttbox} |
|
10 \begin{ttdescription} |
|
11 \item[\ttindexbold{quit}();] ends the Isabelle session, without saving |
|
12 the state. |
|
13 |
|
14 \item[\ttindexbold{exit} \(i\);] similar to {\tt quit}, passing return |
|
15 code \(i\) to the operating system. |
|
16 |
|
17 \item[\ttindexbold{commit}();] saves the current state without ending |
|
18 the session, provided that the logic image is opened read-write; |
|
19 return value {\tt false} indicates an error. |
|
20 \end{ttdescription} |
|
21 |
|
22 Typing control-D also finishes the session in essentially the same way |
|
23 as the sequence {\tt commit(); quit();} would. |
|
24 |
|
25 %%% Local Variables: |
|
26 %%% mode: latex |
|
27 %%% TeX-master: "ref" |
|
28 %%% End: |
|