From: Ron Garret
Subject: Any ACL2 users out there?
Date: 
Message-ID: <gat-796465.11570213082004@nntp1.jpl.nasa.gov>
Is anyone reading this newsgroup using ACL2 (the theorem prover, not 
Allegro Common Lisp 2 (there is no such thing))?  I'm trying to learn 
how to use it, and the documentation is pretty good, but it would be 
handy to be able to ask some questions of an experienced user.

Thanks,
Ron Garret
··········@jpl.nasa.gov
From: Pascal Costanza
Subject: Re: Any ACL2 users out there?
Date: 
Message-ID: <cfj3iq$9dl$1@newsreader2.netcologne.de>
Ron Garret wrote:

> Is anyone reading this newsgroup using ACL2 (the theorem prover, not 
> Allegro Common Lisp 2 (there is no such thing))?  I'm trying to learn 
> how to use it, and the documentation is pretty good, but it would be 
> handy to be able to ask some questions of an experienced user.

They have an excellent mailing list which you should be able to find on 
their website.


Pascal

-- 
Tyler: "How's that working out for you?"
Jack: "Great."
Tyler: "Keep it up, then."