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

Thanks for the answers Michael, Freek, Mark. ___ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info

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

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

The short answer is "no". I'm afraid that working from a script file to do this would require a (more or less general purpose) SML parser as our tactics are just functions, and they are composed together with other SML functions into one overarching SML value. A gross approximation that did pa

[Hol-info] Visualizing subgoals in a proof script

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: ___ hol-info mailing list