.\"                                      Hey, EMACS: -*- nroff -*-
.\" First parameter, NAME, should be all caps
.\" Second parameter, SECTION, should be 1-8, maybe w/ subsection
.\" other parameters are allowed: see man(7), man(1)
.TH PROOFGENERAL 1 "January  6, 2012"
.\" Please adjust this date whenever revising the manpage.
.\"
.\" Some roff macros, for reference:
.\" .nh        disable hyphenation
.\" .hy        enable hyphenation
.\" .ad l      left justify
.\" .ad b      justify to both left and right margins
.\" .nf        disable filling
.\" .fi        enable filling
.\" .br        insert line break
.\" .sp <n>    insert n+1 empty lines
.\" for manpage-specific macros, see man(7)
.SH NAME
proofgeneral \- start Emacs with the Proof General splash screen
.SH SYNOPSIS
.B proofgeneral
.RI "files" ...
.SH DESCRIPTION
The command
.B proofgeneral
is just an abbreviation for 
.I emacs -f proof-splash-display-screen\fR.
Thus it starts emacs, displays the Proof General splash screen
and behaves otherwise identical to emacs. 
.PP
Use
.B proofgeneral
.I file.v
to start Proof General in Coq mode for 
.I file.v\fR.
.SH SEE ALSO
.BR emacs (1),
.SH AUTHOR
The 
.B proofgeneral
script and this manual page were written
by Hendrik Tews <hendrik@askra.de>,
specifically for the Debian project (and may be used by others).