Custom Query (361 matches)
Results (82 - 84 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #201 | fixed | X-Symbol only half enabled (Emacs: yes, prover: no) | ||
| Description |
Linux (SuSE or Ubuntu) and xemacs-21.4.x Running the isabelle-interface script with option -x true (for X-Symbols) does not fully enable xsymbols mode; in the Emacs buffer symbols are rendered as expected, but the prover does not have the "xsymbols" print_mode enabled. After manual disabling and re-enabling in the PG/Options menu, xsymbols work as expected. |
|||
| #202 | fixed | Prover chokes on Unicode Tokens (Carbon Emacs) | ||
| Description |
After a recent change in the unicode token mode, the prover chokes on the text sent by (Carbon) Emacs. Presumably, the tokens are not replaced by their Isabelle symbol equivalents. |
|||
| #204 | fixed | undo stops undoing in large proofs | ||
| Description |
In large Coq proofs (with more than 100 lines), undo stops working. For instance: Lemma Foo : True. idtac. [repeat "idtac." around another 112 times] assert (NI : ~False). intros IX; auto. (* Process the script until here, then undo back 3 or 4 lines.
|
|||
