Abella 1.3.2

[Andrew Gacek]

I'm pleased to announce the release of Abella 1.3.2. The primary
feature in this new version is support for specification modularity
via the lambdaProlog notions of accum_sig and accumulate. To further
support modularity, the import mechanism of Abella has been extended
to allow theorems proved about specifications to be used in contexts
where such specifications are accumulated (subject to the restriction
that no new clauses for existing predicates are introduced).

The new version is available at http://abella.cs.umn.edu/ and a
detailed list of changes follows:

* Added specification modularity via accum_sig and accumulate.

* Loosened the conditions on importing developments to allow
greater use of specification modularity.

* Reorganized the examples directory to have a hierarchical structure.

* Added the -M flag which can be used to generate makefile style
dependency lists for developments. Also added examples/makefile which
demonstrates a typical makefile for a development.

* The search tactic now descends underneath forall and
implication. It now embodies every right rule of the logic.

* A 'witnesses' option has been added to the Set command which
causes search witnesses to be displayed after successful uses of the
search tactic.

* A warning is now issued when Teyjus keywords (which are not used
in Abella) are used in a specification. In all other respects,
specifications in Abella should now be a proper subset of those in
Teyjus. Note that with this change, spaces are required around the =
token.

-Andrew