140 needs to be provided by the user, Isabelle infers the type of all |
140 needs to be provided by the user, Isabelle infers the type of all |
141 variables automatically (this is called \bfindex{type inference}) |
141 variables automatically (this is called \bfindex{type inference}) |
142 and keeps quiet about it. Occasionally this may lead to |
142 and keeps quiet about it. Occasionally this may lead to |
143 misunderstandings between you and the system. If anything strange |
143 misunderstandings between you and the system. If anything strange |
144 happens, we recommend that you ask Isabelle to display all type |
144 happens, we recommend that you ask Isabelle to display all type |
145 information via the Proof General menu item \textsf{Isabelle} $>$ |
145 information via the Proof General menu item \pgmenu{Isabelle} $>$ |
146 \textsf{Settings} $>$ \textsf{Show Types} (see \S\ref{sec:interface} |
146 \pgmenu{Settings} $>$ \pgmenu{Show Types} (see \S\ref{sec:interface} |
147 for details). |
147 for details). |
148 \end{warn}% |
148 \end{warn}% |
149 \index{types|)} |
149 \index{types|)} |
150 |
150 |
151 |
151 |
262 A particular problem for novices can be the priority of operators. If |
262 A particular problem for novices can be the priority of operators. If |
263 you are unsure, use additional parentheses. In those cases where |
263 you are unsure, use additional parentheses. In those cases where |
264 Isabelle echoes your input, you can see which parentheses are dropped |
264 Isabelle echoes your input, you can see which parentheses are dropped |
265 --- they were superfluous. If you are unsure how to interpret |
265 --- they were superfluous. If you are unsure how to interpret |
266 Isabelle's output because you don't know where the (dropped) |
266 Isabelle's output because you don't know where the (dropped) |
267 parentheses go, set the Proof General flag \textsf{Isabelle} $>$ |
267 parentheses go, set the Proof General flag \pgmenu{Isabelle} $>$ |
268 \textsf{Settings} $>$ \textsf{Show Brackets} (see \S\ref{sec:interface}). |
268 \pgmenu{Settings} $>$ \pgmenu{Show Brackets} (see \S\ref{sec:interface}). |
269 \end{warn} |
269 \end{warn} |
270 |
270 |
271 |
271 |
272 \section{Variables} |
272 \section{Variables} |
273 \label{sec:variables} |
273 \label{sec:variables} |
307 \bfindex{Proof General}~\cite{proofgeneral,Aspinall:TACAS:2000}. |
307 \bfindex{Proof General}~\cite{proofgeneral,Aspinall:TACAS:2000}. |
308 Interaction with Isabelle at the shell level, although possible, |
308 Interaction with Isabelle at the shell level, although possible, |
309 should be avoided. Most of the tutorial is independent of the |
309 should be avoided. Most of the tutorial is independent of the |
310 interface and is phrased in a neutral language. For example, the |
310 interface and is phrased in a neutral language. For example, the |
311 phrase ``to abandon a proof'' corresponds to the obvious |
311 phrase ``to abandon a proof'' corresponds to the obvious |
312 action of clicking on the \textsf{Undo} symbol in Proof General. |
312 action of clicking on the \pgmenu{Undo} symbol in Proof General. |
313 Proof General specific information is often displayed in paragraphs |
313 Proof General specific information is often displayed in paragraphs |
314 identified by a miniature Proof General icon. Here are two examples: |
314 identified by a miniature Proof General icon. Here are two examples: |
315 \begin{pgnote} |
315 \begin{pgnote} |
316 Proof General supports a special font with mathematical symbols known |
316 Proof General supports a special font with mathematical symbols known |
317 as ``x-symbols''. All symbols have \textsc{ascii}-equivalents: for |
317 as ``x-symbols''. All symbols have \textsc{ascii}-equivalents: for |
318 example, you can enter either \verb!&! or \verb!\<and>! to obtain |
318 example, you can enter either \verb!&! or \verb!\<and>! to obtain |
319 $\land$. For a list of the most frequent symbols see table~\ref{tab:ascii} |
319 $\land$. For a list of the most frequent symbols see table~\ref{tab:ascii} |
320 in the appendix. |
320 in the appendix. |
321 |
321 |
322 Note that by default x-symbols are not enabled. You have to switch |
322 Note that by default x-symbols are not enabled. You have to switch |
323 them on via the menu item \textsf{Proof-General} $>$ \textsf{Options} $>$ |
323 them on via the menu item \pgmenu{Proof-General} $>$ \pgmenu{Options} $>$ |
324 \textsf{X-Symbols} (and save the option via the top-level |
324 \pgmenu{X-Symbols} (and save the option via the top-level |
325 \textsf{Options} menu). |
325 \pgmenu{Options} menu). |
326 \end{pgnote} |
326 \end{pgnote} |
327 |
327 |
328 \begin{pgnote} |
328 \begin{pgnote} |
329 Proof General offers the \textsf{Isabelle} menu for displaying |
329 Proof General offers the \pgmenu{Isabelle} menu for displaying |
330 information and setting flags. A particularly useful flag is |
330 information and setting flags. A particularly useful flag is |
331 \textsf{Isabelle} $>$ \textsf{Settings} $>$ \textsf{Show Types} which |
331 \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ \pgdx{Show Types} which |
332 causes Isabelle to output the type information that is usually |
332 causes Isabelle to output the type information that is usually |
333 suppressed. This is indispensible in case of errors of all kinds |
333 suppressed. This is indispensible in case of errors of all kinds |
334 because often the types reveal the source of the problem. Once you |
334 because often the types reveal the source of the problem. Once you |
335 have diagnosed the problem you may no longer want to see the types |
335 have diagnosed the problem you may no longer want to see the types |
336 because they clutter all output. Simply reset the flag. |
336 because they clutter all output. Simply reset the flag. |
343 By default, you are in HOL\footnote{This is controlled by the |
343 By default, you are in HOL\footnote{This is controlled by the |
344 \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle System Manual} |
344 \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle System Manual} |
345 for more details.}. |
345 for more details.}. |
346 |
346 |
347 \begin{pgnote} |
347 \begin{pgnote} |
348 You can choose a different logic via the \textsf{Isabelle} $>$ |
348 You can choose a different logic via the \pgmenu{Isabelle} $>$ |
349 \textsf{Logics} menu. For example, you may want to work in the real |
349 \pgmenu{Logics} menu. For example, you may want to work in the real |
350 numbers, an extension of HOL (see \S\ref{sec:real}). |
350 numbers, an extension of HOL (see \S\ref{sec:real}). |
351 % This is just excess baggage: |
|
352 %(You have to restart Proof General if you only compile the new logic |
|
353 %after having launching Proof General already). |
|
354 \end{pgnote} |
351 \end{pgnote} |