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