search

tirix / rumm

A tactics-based Metamath proof language
3 stars 2 forks source link

Reword debug prints and add formula substitution #2

Closed tirix closed 1 year ago

tirix commented 1 year ago

This improves the readability of debug prints by adding indentation. Adds a new "substitution" construct for formulas. A third theorem ellimc can now be proven using the updated tactics.