From efb1c6f2357cb2088ca3a4c75b59523b750398ed Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 28 Sep 2000 12:10:00 +0000
Subject: First (non-working) versions, committed so that doc builds.

---
 acl2/example.acl2 | 14 ++++++++++++++
 1 file changed, 14 insertions(+)
 create mode 100644 acl2/example.acl2

(limited to 'acl2/example.acl2')

diff --git a/acl2/example.acl2 b/acl2/example.acl2
new file mode 100644
index 00000000..e597cd29
--- /dev/null
+++ b/acl2/example.acl2
@@ -0,0 +1,14 @@
+(*
+    Example proof script for ACL2 Proof General.
+
+    $Id$
+*)    
+
+(defthm assoc->assoc-equal
+  (equal (assoc x a)
+	 (assoc-equal x a)))
+
+(defthm assoc->assoc-equal
+  (equal (assoc x a)
+	 (assoc-equal x a)))
+
-- 
cgit v1.2.3