Dear Mario, >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>
For HOL Light there is Mark Adams's "tactician" which I expect would make something like this possible (even though I expect it only would work on the majority of proofs, and not be guaranteed to work on all of them). But that's HOL Light, not HOL4. Freek _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
