-
Notifications
You must be signed in to change notification settings - Fork 2
/
README
52 lines (37 loc) · 2.09 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
============================================================================
prooftree --- proof tree display for Proof General
============================================================================
Prooftree is a program for proof tree visualization during interactive
proof development in Proof General. Currently, it only supports Coq. See
http://askra.de/software/prooftree/ for more information.
This version of prooftree requires Proof General later than March 2021 and
Coq version >= 8.11. These versions of Proof General and Coq must be
installed separately.
============================================================================
USAGE
============================================================================
Start Emacs/Proof General and load any Coq file. Proof display with
prooftree is initially disabled. To enable it, hit the prooftree tool-bar
icon, select menu Proof-General -> Start/Stop Prooftree or type C-c C-d. If
you are inside a proof any of these actions will launch a proof-tree
display for the current proof. Otherwise prooftree will be launched as soon
as you start the next proof. Comprehensive usage information is provided by
the help menu item inside Prooftree and by the Prooftree man page.
============================================================================
CREDITS / CONTACT / COPYRIGHT
============================================================================
Prooftree is more or less a reimplementation of the graphical proof display
of Pvs with a number of enhancements for Coq. The Pvs version is
implemented in Tcl/Tk and controlled directly by the Pvs prover process,
which has some advantages over the prooftree approach.
Please send bug reports, comments, patches, donations to
Hendrik Tews <[email protected]>
Instructions about adding support for a new proof assistant is contained in
the Proof General Adapting manual.
Prooftree is distributed under GPL version 3.
Copyright (C) 2011 - 2024 Hendrik Tews
============================================================================
Local Variables:
mode: indented-text
fill-column: 75
End: