Re: [Hol-info] Visualizing subgoals in a proof script

Hi Mario, Yes, as Freek says, Tactician would do the sort of thing you need, but is only for HOL Light. It works on the vast majority of tactic proofs as they are typically written in HOL Light, say perhaps 1 in every 1,000 proof script lines might trip it up. It could be ported to HOL4, but

Re: [Hol-info] Visualizing subgoals in a proof script

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: > For HOL Light there is Mark Adams's "tactician" which