Hello. In HOL4 is there a way to generate something like the entries in Metamath proof explorer for the subgoals generated within a proof and the tactics used to solve them? Example: <http://us.metamath.org/mpeuni/eluniab.html>
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
