You forgot to mention the comprehensive Vim mode for HOL4. (See tools/vim in the HOL4 repository.)
On 4 November 2015 at 16:22, Joe Leslie-Hurd <j...@gilith.com> 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 ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
