index
:
proof-general
master
Emacs interface for proof assistants
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
hol-light
Commit message (
Expand
)
Author
Age
*
- support bullets and braces in Prooftree
Hendrik Tews
2013-01-15
*
Update
David Aspinall
2012-11-01
*
Remove option aspect of 'finfo' datatype, and rename datatype to 'mldata'.
mark
2012-02-24
*
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-23
*
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-21
*
First version of HOL Light tactic recording.
mark
2012-02-16
*
Add example menu entry
David Aspinall
2012-02-08
*
Duplicate proof
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
*
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-08
*
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
*
Pasto
David Aspinall
2012-02-07
*
Start support for both plain and custom top levels (work in progress).
David Aspinall
2012-02-07
*
Draft symbol handling
David Aspinall
2012-01-23
*
Rename goalstate file for pg
David Aspinall
2012-01-20
*
Rename file
David Aspinall
2012-01-20
*
Hint about changing prompt
David Aspinall
2012-01-20
*
Temporary commit to share file, this is work in progress for Prooftree
David Aspinall
2012-01-19
*
Add file from Mark
David Aspinall
2012-01-19
*
Patch needed temporarily to avoid rebuild of Prooftree
David Aspinall
2012-01-19
*
Update documentation
David Aspinall
2012-01-19
*
Improve configuration for HOL Light. Allow goals display to be prefixed by i...
David Aspinall
2012-01-09
*
Make configuration settings. Tweak error regexp.
David Aspinall
2012-01-06
*
Some fixes to get a working instance for HOL Light. Work in progress.
David Aspinall
2012-01-05
*
Updated
David Aspinall
2010-10-10
*
Experimental hol-light version, not usable yet
David Aspinall
2010-09-29