index
:
proof-general
master
Emacs plugins for proof management systems
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2012-04-06
Fix compile error, Trac #437.
David Aspinall
2012-03-05
remove deprecated desktop keys
Hendrik Tews
2012-03-05
support DESTDIR in make install
Hendrik Tews
2012-03-01
fix compilation with emacs23-nox of Debian
Hendrik Tews
2012-02-24
Remove option aspect of 'finfo' datatype, and rename datatype to 'mldata'.
mark
2012-02-23
Altered graph .dot export so that nodes are displayed as their tactic.
mark
2012-02-23
Allocate jobs!
David Aspinall
2012-02-23
*** empty log message ***
mark
2012-02-23
Capability for exporting .dot files added.
mark
2012-02-21
Various small improvements to capability
mark
2012-02-21
*** empty log message ***
David Aspinall
2012-02-21
*** empty log message ***
David Aspinall
2012-02-21
*** empty log message ***
David Aspinall
2012-02-16
First version of HOL Light tactic recording.
mark
2012-02-13
fix coqdep error recognition
Hendrik Tews
2012-02-10
Fixed an ineficiency in comment detection.
Pierre Courtieu
2012-02-08
Add example menu entry
David Aspinall
2012-02-08
Duplicate proof
David Aspinall
2012-02-08
proof-shell-start: initialise associated buffers before shell mode, so in rig...
David Aspinall
2012-02-08
Tweak output strings and prompt matching
David Aspinall
2012-02-08
Abort attempt to use special exception printing
David Aspinall
2012-02-08
Add print_exn for marked up error messages.
David Aspinall
2012-02-08
Add restart command (does nothing)
David Aspinall
2012-02-08
Add autotest
David Aspinall
2012-02-08
Fix pareno
David Aspinall
2012-02-08
Add hol-light-prog-name, restart command.
David Aspinall
2012-02-08
Try to make evars output match what is expected by Prooftree
David Aspinall
2012-02-08
Test examples for HOL Light
David Aspinall
2012-02-08
Add proof-forget-id command and make top_thm discard the goalstack.
David Aspinall
2012-02-08
Improve handling of undo, implementing pg_kill and pg_undo.
David Aspinall
2012-02-08
More progress with Prooftree. Basic trees produced. Undoing needs work.
David Aspinall
2012-02-08
Adjust global state idea, it is supposed to count down as well as up...
David Aspinall
2012-02-07
Bump year
David Aspinall
2012-02-07
Get a little bit further with proof tree.
David Aspinall
2012-02-07
Load pg_tactics, fix proof-undo-n-times-cmd again.
David Aspinall
2012-02-07
Borrow syntax keywords from caml-mode if available. Typo in undo-n-times.
David Aspinall
2012-02-07
Use right HOL system
David Aspinall
2012-02-07
Attempt to rebind failwith, which fails, with...errors
David Aspinall
2012-02-07
Fix compile
David Aspinall
2012-02-07
New pseudo instances to help tool demonstrators in ocaml/ghci (in progress)
David Aspinall
2012-02-07
Updated.
David Aspinall
2012-02-07
Extend list of provers we compile for
David Aspinall
2012-02-07
Pasto
David Aspinall
2012-02-07
Start support for both plain and custom top levels (work in progress).
David Aspinall
2012-02-07
Cleanup
David Aspinall
2012-02-06
Set version tag for new release.
David Aspinall
2012-02-01
Cleaning some code.
Pierre Courtieu
2012-02-01
Quick fix of a regression introduced by my last commit. Looking for a
Pierre Courtieu
2012-02-01
Fixed command end recognition in presence of operators of the form .+
Pierre Courtieu
2012-01-23
make sure extra modes available
David Aspinall
[next]