It might be useful to have a way to print html files for the immediate dependencies of a statement, similar to how the 'show trace_back /tree /depth <n>' command works. For example along with the proofs of ~syl one could have the proofs of ~a1i and ~mpd, and then proofs of their dependencies, etc. I'm thinking if say you wanted to print out pages of metamath proofs for a course you could do this for several statements, varying the depth parameter to the desired level of detail. However I've tried different syntax and I don't think metamath will do this. Would this be a desirable feature?
Very sorry to hear about Norm's passing.... I never met him in person but he was always there ready to answer even silly questions, and helpful in teaching me concepts whenever I hit a stumbling block. A very good soul. RIP. -- 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 on the web visit https://groups.google.com/d/msgid/metamath/e3196cd7-13ec-4643-9113-667ebe3552f3n%40googlegroups.com.
