19 \end{ttbox} |
19 \end{ttbox} |
20 Note that any Isabelle/Isar command may be retracted by \texttt{undo}. The |
20 Note that any Isabelle/Isar command may be retracted by \texttt{undo}. The |
21 \texttt{help} command prints a list of available language elements. |
21 \texttt{help} command prints a list of available language elements. |
22 |
22 |
23 |
23 |
24 \subsection{The Proof~General interface} |
24 \subsection{Proof~General} |
25 |
25 |
26 Plain TTY-based interaction as above used to be quite feasible with |
26 Plain TTY-based interaction as above used to be quite feasible with |
27 traditional tactic based theorem proving, but developing Isar documents really |
27 traditional tactic based theorem proving, but developing Isar documents really |
28 demands some better user-interface support. David Aspinall's |
28 demands some better user-interface support. David Aspinall's |
29 \emph{Proof~General}\index{Proof General} environment |
29 \emph{Proof~General}\index{Proof General} environment |
33 the current position within a partial proof document is equally important than |
33 the current position within a partial proof document is equally important than |
34 the actual proof state. Thus Proof~General provides the canonical working |
34 the actual proof state. Thus Proof~General provides the canonical working |
35 environment for Isabelle/Isar, both for getting acquainted (e.g.\ by replaying |
35 environment for Isabelle/Isar, both for getting acquainted (e.g.\ by replaying |
36 existing Isar documents) and for production work. |
36 existing Isar documents) and for production work. |
37 |
37 |
38 \medskip |
38 |
|
39 \subsubsection{Proof~General as default Isabelle interface} |
39 |
40 |
40 The easiest way to use Proof~General is to make it the default Isabelle user |
41 The easiest way to use Proof~General is to make it the default Isabelle user |
41 interface (see also \cite{isabelle-sys}). Just put something like this into |
42 interface (see also \cite{isabelle-sys}). Just put something like this into |
42 your Isabelle settings file: |
43 your Isabelle settings file: |
43 \begin{ttbox} |
44 \begin{ttbox} |
73 Users of XEmacs may note the tool bar for navigating forward and backward |
74 Users of XEmacs may note the tool bar for navigating forward and backward |
74 through the text. Consult the Proof~General documentation \cite{proofgeneral} |
75 through the text. Consult the Proof~General documentation \cite{proofgeneral} |
75 for further basic command sequences, such as ``\texttt{C-c C-return}'' or |
76 for further basic command sequences, such as ``\texttt{C-c C-return}'' or |
76 ``\texttt{C-c u}''. |
77 ``\texttt{C-c u}''. |
77 |
78 |
78 \medskip |
79 |
|
80 \subsubsection{The X-Symbol package} |
79 |
81 |
80 Proof~General also supports the Emacs X-Symbol package \cite{x-symbol}, which |
82 Proof~General also supports the Emacs X-Symbol package \cite{x-symbol}, which |
81 provides a nice way to get proper mathematical symbols displayed on screen. |
83 provides a nice way to get proper mathematical symbols displayed on screen. |
82 Just pass option \texttt{-x true} to the Isabelle interface script, or check |
84 Just pass option \texttt{-x true} to the Isabelle interface script, or check |
83 the appropriate menu setting by hand. In any case, the X-Symbol package must |
85 the appropriate menu setting by hand. In any case, the X-Symbol package must |
84 have been properly installed already. |
86 have been properly installed already. |
85 |
87 |
86 Note that using actual mathematical symbols in the text easily makes the ASCII |
88 Contrary to what you may expect from the documentation of X-Symbol, the |
87 sources hard to read. For example, $\forall$ will appear as \verb,\\<forall>, |
89 package is very easy to install for individual users and configures itself |
88 according the default set of Isabelle symbols. On the other hand, the |
90 automatically. Simply download the ``binary'' package file, and do something |
89 Isabelle document preparation system \cite{isabelle-sys} will be happy to |
91 like this to install it in your home directory: |
90 print non-ASCII symbols properly. It is even possible to invent additional |
92 \begin{ttbox} |
91 notation beyond the display capabilities of XEmacs and X-Symbol. |
93 mkdir -p ~/.xemacs |
|
94 cd ~/.xemacs |
|
95 tar xzf .../x-symbol-pkg.tar.gz |
|
96 \end{ttbox} |
|
97 |
|
98 \medskip |
|
99 |
|
100 Using proper mathematical symbols in Isabelle theories can be very convenient |
|
101 for readability of large formulas. On the other hand, the plain ASCII sources |
|
102 easily become somewhat unintelligible. For example, $\forall$ will appear as |
|
103 \verb,\\<forall>, according the default set of Isabelle symbols. |
|
104 Nevertheless, the Isabelle document preparation system (see |
|
105 \S\ref{sec:document-prep}) will be happy to print non-ASCII symbols properly. |
|
106 It is even possible to invent additional notation beyond the display |
|
107 capabilities of XEmacs and X-Symbol. |
92 |
108 |
93 |
109 |
94 \section{Isabelle/Isar theories} |
110 \section{Isabelle/Isar theories} |
95 |
111 |
96 Isabelle/Isar offers the following main improvements over classic Isabelle. |
112 Isabelle/Isar offers the following main improvements over classic Isabelle. |
134 Porting of existing tactic scripts is best done by running two separate |
150 Porting of existing tactic scripts is best done by running two separate |
135 Proof~General sessions, one for replaying the old script and the other for the |
151 Proof~General sessions, one for replaying the old script and the other for the |
136 emerging Isabelle/Isar document. |
152 emerging Isabelle/Isar document. |
137 |
153 |
138 |
154 |
139 \subsection{Document preparation} |
155 \subsection{Document preparation}\label{sec:document-prep} |
140 |
156 |
141 Isabelle/Isar provides a simple document preparation system based on current |
157 Isabelle/Isar provides a simple document preparation system based on current |
142 (PDF) {\LaTeX} technology, with full support of hyper-links (both local |
158 (PDF) {\LaTeX} technology, with full support of hyper-links (both local |
143 references and URLs), bookmarks, thumbnails etc. Thus the results are equally |
159 references and URLs), bookmarks, thumbnails etc. Thus the results are equally |
144 well suited for WWW browsing and as printed copies. |
160 well suited for WWW browsing and as printed copies. |