> In metamath version 0.192 ( http://us2.metamath.org/index.html#mmprog ), "write source" has a new qualifier, "/extract <label-list>", > which will create a self-contained database containing exactly and only the axioms and theorems needed to prove <label-list> > A possible use for this is to create a miniature local website for the extracted xyz.mm, which can be used as a self study guide
Very nice feature Glauco -- 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/3144edd1-9acd-4419-8ccb-c474e635d561n%40googlegroups.com.
