.\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.35.
.TH PROOFGENERAL "1" "August 2005" "proofgeneral ()" "User Commands"
.SH NAME
proofgeneral \- manual page for proofgeneral ()
.SH SYNOPSIS
.B proofgeneral
[\fIOPTION\fR] [\fIFILE\fR]...
.SH DESCRIPTION
Launches Emacs Proof General, editing the proof script FILE.
.SH OPTIONS
.TP
\fB\-\-emacs\fR
startup Proof General with emacs (GNU Emacs)
.TP
\fB\-\-xemacs\fR
startup Proof General with xemacs (XEmacs)
.TP
\fB\-\-emacsbin\fR <EMACS>
startup Proof General with emacs binary <EMACS>
.TP
\fB\-h\fR, \fB\-\-help\fR
show this help and exit
.TP
\fB\-v\fR, \fB\-\-version\fR
output version information and exit
.PP
Unrecognized options are passed to Emacs, along with file names.
.SH EXAMPLES
.TP
proofgeneral Example.thy
Load Proof General editing Isar file Example.thy
.TP
proofgeneral example.v
Load Proof General editing Coq file Example.v
.PP
For documentation and latest versions, visit http://proofgeneral.inf.ed.ac.uk.
.SH "REPORTING BUGS"
Report bugs to <da+pg\-bugs@inf.ed.ac.uk>.
.PP
David Aspinall.
.SH COPYRIGHT
Copyright \(co 1998-2005 LFCS, University of Edinburgh, UK.
.br
This is free software; see the source for copying conditions.
.SH "SEE ALSO"
The full documentation for
.B proofgeneral
is maintained as a Texinfo manual.  If the
.B info
and
.B proofgeneral
programs are properly installed at your site, the command
.IP
.B info proofgeneral
.PP
should give you access to the complete manual.