PROOFGENERAL(1)

NAME
proofgeneral - manual page for proofgeneral ()

SYNOPSIS
proofgeneral [OPTION] [FILE]...

DESCRIPTION
Launches Emacs Proof General, editing the proof script FILE.

OPTIONS

--emacs
    startup Proof General with emacs (GNU Emacs)

--xemacs
    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.

EXAMPLES

proofgeneral Example.thy
    Load Proof General editing Isar file Example.thy

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.

COPYRIGHT
Copyright © 1998-2005 LFCS, University of Edinburgh, UK.
This is free software; see the source for copying conditions.

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.