From 18de9e47c089594762123ef8f9a80428aba7eef8 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Sat, 13 Nov 1999 13:52:52 +0000
Subject: Test case

---
 etc/lego/unsaved-goals.l | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 etc/lego/unsaved-goals.l

(limited to 'etc/lego')

diff --git a/etc/lego/unsaved-goals.l b/etc/lego/unsaved-goals.l
new file mode 100644
index 00000000..55275eca
--- /dev/null
+++ b/etc/lego/unsaved-goals.l
@@ -0,0 +1,23 @@
+(* 
+  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) 
+*)
+   
+
+
+Module unsaved Import lib_logic;
+
+Goal {A,B:Prop}(and A B) -> (and B A);
+intros;
+Refine H;
+intros;
+andI;
+Immed;
+
+[Pred = [s:Type]s->Prop];
+
+Goal {A,B:Prop}(and A B) -> (and B A);
+
-- 
cgit v1.2.3