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 parenthesis-aware lexing of the >>/THEN/\\ operators might achieve pretty good results in practice however.
For purposes such as this, and others, I'm generally interested in the idea of defining a much simpler tactic language (a "DSL" I suppose) that would be easier to parse and analyse. Best wishes, Michael On 2/8/20, 05:36, "Mario Xerxes Castelán Castro «Ksenia»" <marioxcc...@yandex.com> wrote: 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 _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
