summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/System/basics.tex

changeset 7861 | 8d5d3163fd81 |

parent 7849 | 29a2a1d71128 |

child 7882 | 52fb3667f7df |

equal
deleted
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. |