File: README

package info (click to toggle)
prooftree 0.13-1
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, sid, stretch
  • size: 592 kB
  • ctags: 668
  • sloc: ml: 4,462; sh: 117; makefile: 111
file content (54 lines) | stat: -rw-r--r-- 2,162 bytes parent folder | download
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
53
54
============================================================================
           prooftree --- proof tree display for Proof General
============================================================================


Prooftree is a program for proof tree visualization during interactive
proof development in a theorem prover. It is currently being developed for
Coq and Proof General. See http://askra.de/software/prooftree/ for more
information.

Prooftree requires Proof General >= 4.3pre130327 and 
Coq version >= 8.4beta. These versions of Proof General and Coq must be
installed separately. Binary packages are available Debian Jessie, for
instance.


============================================================================
  USAGE
============================================================================

Start Emacs 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. 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 <prooftree@askra.de>

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 - 2016 Hendrik Tews


============================================================================

Local Variables:
mode: indented-text
fill-column: 75
End: