Wanted Features for Proof General in Emacs

Please add your ideas/votes to suggested features below, in each of the categories.

Additional Support for Existing Provers

Do you wish you had extra theorem-prover specific support, such as menus or browsing for keywords, templates, theorems, etc?

Support for New Thoerem Provers

Is there anything that is needed to support your own theorem prover that Proof General can't handle?

High-level Editing Support

Would you like Proof General to support high-level operations for maintaining proof scripts, such as moving theorems and definitions between files, or renaming them? We are researching the ideas of ProofEngineering to help support such high-level editing. Please comment with any suggestions or ideas.

Other ideas