First (non-working) versions, committed so that doc builds.

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:
+