Hi Ender,
/what script could expand a proof fast on-demand to its steps with full statements written down/
Metamath-knife also has the option -e to output the full proof of a single statement in MMP format (with steps in ASCII, not as S-expressions), as a file. Here again since the tool is thought as a library, it would be easy to customize. (Sorry for spamming, I should have answered both points in a single mail) BR, _ Thierry -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/f1f0379a-0bb9-4dc0-8fe8-3e5ce36c3984%40gmx.net.
