HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
630 stars 142 forks source link

emacs mode: package the lisp code for it to be released in a package archive #1103

Open chenzhawyang opened 1 year ago

chenzhawyang commented 1 year ago

maybe it will help to package hol-mode.el and release it on elpa/melpa/nongnu or what have you. both hol and hol-mode are mature enough, this should require minimal work only.

mn200 commented 1 year ago

Sounds a nice idea!