394 interface runs \texttt{isabelle} within its own \textsl{xterm} window. |
394 interface runs \texttt{isabelle} within its own \textsl{xterm} window. |
395 Usually, display of mathematical symbols from the Isabelle font is also |
395 Usually, display of mathematical symbols from the Isabelle font is also |
396 enabled (see \S\ref{sec:tool-installfonts} for font configuration issues). |
396 enabled (see \S\ref{sec:tool-installfonts} for font configuration issues). |
397 Furthermore, different kinds of identifiers in logical terms are highlighted |
397 Furthermore, different kinds of identifiers in logical terms are highlighted |
398 appropriately, e.g.\ free variables in bold and bound variables underlined. |
398 appropriately, e.g.\ free variables in bold and bound variables underlined. |
399 There are some more options available. Just pass \texttt{-?} to the |
399 There are some more options available, just pass ``\texttt{-?}'' to get the |
400 \texttt{xterm} interface to have its usage printed. |
400 usage printed. |
401 |
401 |
402 \medskip Proof~General\index{user interface!Proof General} is a much more |
402 \medskip Proof~General\index{user interface!Proof General} is a much more |
403 advanced interface. It supports both classic Isabelle (as |
403 advanced interface. It supports both classic Isabelle (as |
404 \texttt{ProofGeneral/isa}) and Isabelle/Isar (as \texttt{ProofGeneral/isar}). |
404 \texttt{ProofGeneral/isa}) and Isabelle/Isar (as \texttt{ProofGeneral/isar}). |
405 Note that the latter is slightly better supported, and more robust. |
405 Note that the latter is slightly better supported, and more robust. |