Your company here — click to reach over 10,000 unique daily visitors

proofgeneral - Man Page

manual page for proofgeneral ()


proofgeneral [OPTION] [FILE]...


Launches Emacs Proof General, editing the proof script FILE.



startup Proof General with emacs (GNU Emacs)


startup Proof General with xemacs (XEmacs)

--emacsbin <EMACS>

startup Proof General with emacs binary <EMACS>

-h,  --help

show this help and exit

-v,  --version

output version information and exit

Unrecognized options are passed to Emacs, along with file names.


proofgeneral Example.ec

Load Proof General editing EasyCrypt file Example.ec

proofgeneral example.v

Load Proof General editing Coq file Example.v

For documentation and latest versions, visit http://proofgeneral.inf.ed.ac.uk.

Reporting Bugs

Report bugs to <da+pg-bugs@inf.ed.ac.uk>.

David Aspinall.

See Also

The full documentation for proofgeneral is maintained as a Texinfo manual.  If the info and proofgeneral programs are properly installed at your site, the command

info proofgeneral

should give you access to the complete manual.


August 2005 proofgeneral ()