Abella 1.2 Release
Andrew Gacek
I have just released Abella 1.2 which is aimed at supporting larger
developments. Most notably, it introduces a way to compile and import
developments. This requires a change to way specifications are
associated with developments which is not backwards compatible. All of
the examples have been updated to this new style.
* Specifications are now explicitly loaded into a development via
the Specification command.
* Developments may now be compiled and imported into other developments.
* The Query command allows the animation of definitions.
* Command line options have been reorganized. Run abella --help to
find out more.
* Some run-time options may be configured via the Set command.
* Subgoals now use hierarchical numbering.
* Large hypotheses may now be abbreviated using the abbrev and
unabbrev commands.
* Multi-line comments are now supported via /* ... */. These
comments may be nested.
* The annotations for co-induction now use # and + to avoid
confusion with the annotations for induction (@ and *).
More information is available at
http://abella.cs.umn.edu/changelog.html
And the new version is available as always from
-Andrew