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
