Add "witness" as a synonym of the "exists" tactic.

This allows it to be colorized properly as there is no
shared keyword between formulas and tactics.
Stop printing instantiated variables in the variables list
Fixed a bug about subordination.

Previously, a term of type T can contain a subterm of type T' only
if T' is subordinate to T. This constraint is applied even if T is not
explicitly closed by the "close" command. With the restriction you
cannot, for example, construct a term of type "ty" that contains
a term of type "tm" using the following signature because "tm" is
not subordinate to "ty":

Kind tm, ty type.
Type app   tm -> tm -> tm.
Type abs   (tm -> tm) -> tm.
Type arr   ty -> ty -> ty.

With this bug fix, the constraint above is checked only if T is closed
explicitly.
Extend the stratification checker to complain about higher-order arguments

The following definitions now cause warnings:

    Define bad : prop -> prop by
      bad P := bad P -> false.

    Define ugly : prop by
      ugly := (ugly -> false) -> false.

    Define not : prop -> prop by
      not P := P -> false.

    Define r1 : prop -> prop by
      r1 P := P.  /* no warning here */

    Define r2 : prop -> prop by
      r2 P := r1 P -> false.

The compile-time flag Abella.stratification_warnings_are_errors
can be used to turn stratification warnings into errors. Currently
this is set to "false" for backwards compatibility.
Merge pull request #28 from chaudhuri/ho_stratification

Extend the stratification checker to complain about higher-order arguments
Add support for unfolding named clauses in the spec.

Clauses are named as follows:

   %:name:
   head :- body.

The name must be an identifier between %: and :, and it must be a line
comment. Anything else is a lexical error.