From 59a0979b85debc0deae2bea07765bf29ade9b9d3 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 6 Oct 1999 11:11:38 +0000
Subject: Updated

---
 CHANGES | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index bc7754ca..4a5ee759 100644
--- a/CHANGES
+++ b/CHANGES
@@ -76,9 +76,14 @@ Coq Changes
 Isabelle and Isar Changes
 -------------------------
 
-* Tweaks for input syntax.  
+* Several tweaks for input syntax.  
 
 * Recognize goals of the old form val prems = goal ...
+  and saves of the old form val thm = result.
+
+* Proofs which are "unfinished", i.e. have no qed or result,
+  are now closed off automatically when a new goal is begun,
+  mirroring the behaviour of Isabelle.
 
 
 Only in the developers' release
-- 
cgit v1.2.3