aboutsummaryrefslogtreecommitdiffhomepage
path: root/acl2/README
diff options
context:
space:
mode:
Diffstat (limited to 'acl2/README')
-rw-r--r--acl2/README30
1 files changed, 30 insertions, 0 deletions
diff --git a/acl2/README b/acl2/README
new file mode 100644
index 00000000..961e287a
--- /dev/null
+++ b/acl2/README
@@ -0,0 +1,30 @@
+ACL2 Proof General, for ACL2.
+
+Written by David Aspinall.
+
+$Id$
+
+Status: not officially supported yet
+Maintainer: volunteer required
+ACL2 version: Tested briefly with
+ACL2 homepage:
+
+========================================
+
+
+This is a "technology demonstration" of Proof General for ACL2.
+
+It has basic script management support, with a little bit of
+decoration of scripts and output.
+
+There is support for X Symbol, but not using a proper token language.
+
+I have written this in the hope that somebody from the ACL2 community
+will adopt it, maintain and improve it, and thus turn it into a proper
+instantiation of Proof General.
+
+
+------------
+
+Notes:
+