Abella 1.3.4
Andrew Gacek
I've just released Abella 1.3.4. The new version is available at
http://abella.cs.umn.edu/ and a detailed list of changes follows:
* Added subordination and the Close command. This makes many
pruning lemmas unnecessary, such as showing that a term of type tm
cannot appear inside a term of type nat. See the following page for
details:
http://abella.cs.umn.edu/reference-guide.html#subordination
* Added case analysis on flex-rigid equalities. For example, one
can perform case analysis on an equality like R N = plus A B. The
result is that one step of Huet's algorithm is performed (computing
the possible imitation and projections) and for each result the
standard pattern unification code is called.
* Fixed a unification issue involving the occurs check.
-Andrew