doc-src/System/basics.tex
 changeset 7861 8d5d3163fd81 parent 7849 29a2a1d71128 child 7882 52fb3667f7df
equal inserted replaced
7860:7819547df4d8 7861:8d5d3163fd81
   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.