search

digama0 / mmj2

mmj2 GUI Proof Assistant for the Metamath project
GNU General Public License v2.0
72 stars 25 forks source link

Various updates to the tutorial #20

Closed david-a-wheeler closed 4 years ago

david-a-wheeler commented 4 years ago

As I get into this, I realized that a number of things in the tutorial no longer work as documented, so I made a number of changes in chapter 4 so that it actually works. I also added more information about unification and in particular its "Derive" capability.

Signed-off-by: David A. Wheeler dwheeler@dwheeler.com

david-a-wheeler commented 4 years ago

@digama0 - please merge, or tell me what's wrong with it so I can fix it :-).