v0.0.1

Proof-object generator for unification and antiunification in ML:

• proof-object generation for unification uses the Martelli-Montanari syntactic unification algorithm;
• proof-object generation for antiunification uses the Plotkin algorithm for antiunification;
• proof-objects are based on the (Applicative) ML proof system and some derived rules.