Proposed new feature: Provers

[Rahul Sundaram]

David A. Wheeler wrote:
> Can anyone help us package some additional programs?
> Some potential ones include:
> * ACL2 (I have a start at this, it's written in Common Lisp)
> * haRVey-FOL (depends on E and SPASS)
> * BLAST, at http://mtc.epfl.ch/software-tools/blast/ (don't use the obsolete version at Berkeley)
> * HOL 4
> * Isabelle
> * HOL Lite
> * Gandalf
> * NuSMV
> * DiVinE
> * KeY
>   
It would be quite useful if you add more information, classify them as 
easy, medium, hard similar to the OLPC packages wishlist, the language 
being used etc. I saw them on the packager wishlist and went through a 
couple which seemed a large amount of pain to package.  I am wondering 
if all of these are in the similar category.

Rahul