diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-05-26 14:00:13 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-05-26 14:00:13 +0000 |
| commit | d7b933b0bf2ced8d6f4e46bbfa1f90c53a7dd088 (patch) | |
| tree | cbe1823ec6cea3d13916085ada6be7e4a41a782c /CHANGES | |
| parent | 5ca24c4d1c683f71312831cb4f2b913a961d5030 (diff) | |
Updated
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 16 |
1 files changed, 12 insertions, 4 deletions
@@ -2,15 +2,23 @@ * Summary of Changes for Proof General 4.0 from 3.7.X +** Isabelle/Isar changes + +*** Electric terminator works, without inserting terminator + + ** Generic changes *** XEmacs is no longer supported; PG only works with GNU Emacs 22.2+ *** Font-lock based Unicode Tokens mode replaces X-Symbol -*** Removed configuration options +*** Removed user configuration options proof-toolbar-use-button-enablers (now always enabled) -*** Electric terminator configurable to not insert terminator - This is the default behaviour for Isar with electric terminator - (semicolon is more convenient than C-c C-RET or C-c C-n). +*** Altered prover configuration settings + pg-insert-output-as-comment-fn: removed + proof-shell-strip-output-markup: required for cut-and-paste + proof-electric-terminator-noterminator: allows non-insert of terminator + + |