This is interesting and quite useful! Thank you for sharing. It should be possible to make it compatible with the commonly used tuareg mode. (There are some conflicting keyboard shortcuts and the tuareg mode window is named *caml-toplevel* instead of *shell*.)
Jump-to-proof-point is quite nice! I'm curious how well it works with more complicated proofs e.g. compared to Tactician (http://www.proof-technologies.com/tactician/index.html). Regards, Petros On 04/11/2015 05:22, Joe Leslie-Hurd wrote: > For those of you who use HOL Light in an Emacs shell, I wrote some > simple Emacs Lisp macros to support interactive proof: > > https://github.com/gilith/hol-light-emacs > > It's just basic stuff, but I have found that they speed up proof > development (and the jump-to-proof-point is a boon to proof > maintenance). > > These macros fill a gap between more comprehensive efforts: Michael > Norrish's hol-mode for interacting with HOL4 in Emacs, and Freek > Wiedijk's vi mode for HOL Light. > > Cheers, > > Joe > > ------------------------------------------------------------------------------ > _______________________________________________ > hol-info mailing list > hol-info@lists.sourceforge.net > https://lists.sourceforge.net/lists/listinfo/hol-info > -- Petros Papapanagiotou, Ph.D. CISA, School of Informatics The University of Edinburgh Email: p...@ed.ac.uk --- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
