"(interactive tools for developing formal proofs)" is OK except that it is missing the "Mathematics" keyword, which seems important (assuming that all this is about software that's useful only in mathematics....which I have no clue about.
Everybody in the field of theorem proving will know the Proof General, so there is not so much need to "define" what it is for this group of people. They will look for proof general and will find it directly.
For those who don't, but maybe look for useful mathematical tools, something like "Major mode to turn Emacs into a interactive proof assistent to write formal mathematical proofs using a variety of theorem provers" would give IMO enough information to get an idea what the package is.
Regards Stefan
Attachment:
PGP.sig
Description: Signierter Teil der Nachricht