proof-nested-goals-allowed -> proof-completed-proof-behaviour

Patch for more flexible handling of closing goal...save regions
after proof has been completed.

1 files changed, 38 insertions, 7 deletions

diff --git a/etc/lego/unsaved-goals.l b/etc/lego/unsaved-goals.l
index 55275eca..dd9c9646 100644
--- a/etc/lego/unsaved-goals.l
+++ b/etc/lego/unsaved-goals.l
@@ -1,9 +1,34 @@
 (* 
-  test case for closing off unsaved goals:
-  P.G. should close Goal->Immed even though there
-  is no Save.  Pred definition should not be
-  part of closed region  
-  (test with undoing and redoing) 
+  Some test cases for closing off unsaved goals, 
+  and the setting proof-completed-proof-behaviour.
+
+  David Aspinall, November 1999.
+
+  Things work fairly well in lego with 
+
+       proof-completed-proof-behaviour='closeany
+
+  In that case, undoing/redoing later declarations 
+  (E and F) following the completed proof works okay, and
+  in the absence of declarations, things work fine.
+    
+  Declarations in LEGO are global, and forgetting a
+  declaration when a proof is still open (even if complete)
+  aborts the proof!  So a proper handling would need to
+  trigger a *further* retraction when the "Forget D" is
+  issued undoing the definition of D.  Never mind.
+
+  With proof-completed-proof-behaviour='closegoal or 'extend,
+  undoing the first goal doesn't forget the declarations.
+
+  This file even causes internal errors in LEGO!
+
+     Warning: forgetting a finished proof
+
+     LEGO detects unexpected exception named "InfixInternal"
+
+  Test with undoing and redoing, and various settings
+  for proof-completed-proof-behaviour
 *)
    
 
@@ -16,8 +41,14 @@ Refine H;
 intros;
 andI;
 Immed;
-
-[Pred = [s:Type]s->Prop];
+[D = Type];
+[E = Type];
+[F = Type];
 
 Goal {A,B:Prop}(and A B) -> (and B A);
+intros;
+Refine H;
+intros;
+andI;
+Immed;