Hi Petros, > 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*.)
I was thinking of a lightweight HOL Light mode that highlighted quoted terms/tacticals/etc and knew about indentation of tactic proofs, rather than extending an OCaml mode that has a lot of features that don't really apply to HOL Light tactic proofs. > 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). I have never used tactician, and would be curious how these simple macros compare. Cheers, Joe ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
