From 0d3c430f178c9cc9867a349d535a4a53dea551c2 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 25 Nov 1998 13:03:39 +0000
Subject: note about incomplete goal..save sequences.

---
 todo | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/todo b/todo
index 06752c2a..4caa2796 100644
--- a/todo
+++ b/todo
@@ -205,6 +205,18 @@ C (Isabelle) Messages in minibuffer appear in FSF Emacs with ugly ^J's.
   Generic problem, really: maybe CRs should be stripped, and just first
   line of multiline urgent message displayed in minibuffer.
 
+D Perhaps goal..save sequences should be closed also by the appearance
+  of a new goal, even though this may be a "broken" proof.  At the
+  moment, undoing past the new goal causes errors:
+  
+     <goal>
+     ...
+     <new goal>
+     ..
+
+  Will ACS idea handle this?
+  
+
 D Better support for adding a new prover: give error messages which
   hint at what variable to set (see proof-issue-goal for example).
 
-- 
cgit v1.2.3