proofgeneral (1) Linux Manual Page
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 [at] 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.