GitHub - hide-kawabata/proof-tree: proof tree display for Proof General

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 199 Commits
debian		debian
test		test
.gitattributes		.gitattributes
.gitignore		.gitignore
COPYING		COPYING
ChangeLog		ChangeLog
INSTALL		INSTALL
Makefile.in		Makefile.in
README		README
about_window.ml		about_window.ml
changes.html		changes.html
compatibility		compatibility
configuration.ml		configuration.ml
configure		configure
coq.ml		coq.ml
draw_tree.ml		draw_tree.ml
emacs_commands.ml		emacs_commands.ml
ext_dialog.ml		ext_dialog.ml
gtk_ext.ml		gtk_ext.ml
help_window.ml		help_window.ml
input.ml		input.ml
input.mli		input.mli
main.ml		main.ml
make-deb-package		make-deb-package
make-release		make-release
node_window.ml		node_window.ml
proof_tree.ml		proof_tree.ml
proof_tree.mli		proof_tree.mli
proof_window.ml		proof_window.ml
prooftree.1		prooftree.1
tree_layers.ml		tree_layers.ml
util.ml		util.ml
version.mli		version.mli
version.txt		version.txt

Repository files navigation

============================================================================
           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: