From ef1b6fd069272733ee9f06ba03215ef7702a1aa8 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 11 Jun 2002 10:54:52 +0000
Subject: New files.

---
 etc/coq/nested.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 etc/coq/nested.v

diff --git a/etc/coq/nested.v b/etc/coq/nested.v
new file mode 100644
index 00000000..db7608ea
--- /dev/null
+++ b/etc/coq/nested.v
@@ -0,0 +1,19 @@
+(*
+    Example nested proof script for testing support of nested proofs.
+*)
+
+Goal (A,B:Prop)(A /\ B) -> (B /\ A).
+  Intros A B H.
+  Induction H.
+  Apply conj.
+  Lemma foo: (A,B:Prop)(A /\ B) -> (B /\ A).
+    Intros A B H.
+    Induction H.
+    Apply conj.
+    Assumption.
+    Assumption.
+  Save.
+  Assumption.
+  Assumption.
+Save and_comms.
+
-- 
cgit v1.2.3