Release notes for Twelf 1.3

Major internal update to Twelf 1.2, available as alpha release.

Externall visible changes:

- Constraints

Type reconstruction and the logic programming engine (but not yet
the theorem prover) allow various constraint domains in the style
of constraint logic programming languages.  The main ones are
equalities and inequalities over rationals and integers.

- Tracing and Breakpoints

The logic programming engine now support tracing and setting of
breakpoints for illustration and debugging purposes.

- Theorem Prover

The theorem prover now allows quantification over regular context.  The
theorem prover will also use previously proved theorems with %prove) and
ignore those with %establish, which is otherwise equivalent.  In unsafe
mode, %assert can be used to claim theorems.  However, at present no
longer generates proof terms.

- Reduction Checking

The termination checker has been extended to verify if output arguments
to a predicate are smaller than some inputs with the %reduces
declaration.

- Signature Printing

Signatures can now be printed, also in TeX format.

- Abbreviations

Added abbreviations (%abbrev) which, unlike definition, do not need to
be strict.

- Name Preferences

Name preference declarations (%name) now allow an optional second
argument for naming of parameters.