From d4316a2d63c9c2b12cdce73e62cd435d7ff01002 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 6 Oct 1999 11:18:56 +0000
Subject: More improvements/fixes for closing unfinished proofs. Added
 proof-unnamed-theorem-name.

---
 CHANGES | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index d5e9787d..8f1c4475 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,6 +7,10 @@ Generic Changes
 * New function C-c C-f (proof-find) to invoke some prover-specific
   mechanism to search for theories.  
 
+* Whenever scripting is triggered in a new file, a cd command
+  is sent to the proof assistant to switch to the right directory
+  (in case other files are included).
+
 * [XEmacs only] Toolbar has six new buttons (State, Context, Info, 
   Command, Help, Stop) which invoke commands previously available on 
   keys/menus.   Also a new "Find" button for proof-find.
@@ -73,6 +77,13 @@ Coq Changes
   specific command C-c C-s (coq-Search).
 
 
+LEGO Changes
+------------
+
+* Proofs which have no save command are now closed off automatically
+  when a new goal is begun, mirroring the behaviour of LEGO.
+
+
 Isabelle and Isar Changes
 -------------------------
 
@@ -117,10 +128,16 @@ Internal changes for developers to note
   using special character codes is fragile and needs replacing
   in future versions of Proof General!
 
+* Proofs which are "unfinished", i.e. have no qed or result,
+  are now closed off automatically when a new goal is begun.
+  The new code only applies if proof-nested-goals-allowed is
+  nil (the default).  Setting this variable to t forces 
+  identical behaviour to before.  The default for Coq is t.
+
 * Renamed some configuration variables for uniformity:
     proof-ctxt-string -> proof-context-command
     proof-help-string -> proof-info-command
     proof-prf-string  -> proof-showproof-command
 
-* Code cleanups and improvements.
+* Many code cleanups and improvements.
 
-- 
cgit v1.2.3