I just wanted to share that thanks to Thibault Gauthier, holyhammer (integrated powerful ATP provers) is already quite useful in HOL4.
I put this in my .hol_config: fun hh_tac g = (holyHammer.hh[](list_mk_imp g); ALL_TAC g); Then I can run hh_tac when I get stuck at a goal but think it should be provable by a bunch of first-order reasoning over things in the standard libraries, and if it succeeds it tells me what to pass to metis. N.B. you need to install your own first-order provers. See src/holyhammer for instructions. (To come is better ability to incorporate theorems from the tip of your own development.)
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
