New files.

1 files changed, 62 insertions, 0 deletions

diff --git a/doc/proofgeneral.1 b/doc/proofgeneral.1
new file mode 100644
index 00000000..817bf469
--- /dev/null
+++ b/doc/proofgeneral.1
@@ -0,0 +1,62 @@
+.\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.29.
+.\" Well, actually, it was edited after that by me, so the dire
+.\" warning should not be greatly feared.
+.\" This is based on the output of: help2man ../bin/proofgeneral
+.\"
+.\" $Id$
+.\"
+.TH PROOFGENERAL "1" "March 2004" "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
+.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 AUTHOR
+David Aspinall.
+.SH "REPORTING BUGS"
+Report bugs to <da+pg-bugs@inf.ed.ac.uk>.
+.SH COPYRIGHT
+Copyright \(co 1998-2004 LFCS, University of Edinburgh, UK.
+.br
+This is free software; see the source for copying conditions.
+.SH "SEE ALSO"
+The full documentation for Proof General is available within
+the program, and also as the Texinfo manual.  This should be
+available by the command
+.IP
+.B info ProofGeneral
+.PP
+if the info file has been installed.  There is a second
+manual containing instructions on adapting Proof General
+to new proof assistants:
+.IP
+.B info PG-adapting
+.PP
+Ordinary users do not need to consult this manual.