Metamath-lamp version 17 includes the following updates: The major update is how mm-lamp handles discouraged assertions. Discouraged assertions were supported in the previous versions too, but in version 17 it became more convenient. Also, assertions can be marked as "deprecated". This allows to exclude them from proofs independently of "discouraged" ones. More details on that may be found in the below issues:
"By default ignore any statements marked (New usage is discouraged.)" https://github.com/expln/metamath-lamp/issues/31#issuecomment-1682725469 "By default don't use discouraged syntax nor later syntax" https://github.com/expln/metamath-lamp/issues/108 "Add transitively skipped assertions option" https://github.com/expln/metamath-lamp/issues/152 And few minor changes: "In explorer allow selection of final type" https://github.com/expln/metamath-lamp/issues/111 "Duplicate up button" https://github.com/expln/metamath-lamp/issues/154 "When substituting, always use the most recent selections" https://github.com/expln/metamath-lamp/issues/155 - Igor -- 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/73705bde-76b5-44b1-ad5c-ca98755b1c4an%40googlegroups.com.
