From d7b933b0bf2ced8d6f4e46bbfa1f90c53a7dd088 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 26 May 2009 14:00:13 +0000 Subject: Updated --- CHANGES | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index a4881953..28dfbe11 100644 --- a/CHANGES +++ b/CHANGES @@ -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 + + -- cgit v1.2.3