Typing of quantified expressions and manifest predicates implemented

	modified:   parser.mly
	modified:   support.ml
	modified:   typer.ml
Implemented typing of untyped predicate or function variables

Typical example

    * (pp:G??): ghost G?
        ensure
            Result = {x: all(p) pp(p) => p(x)}
        end

Suppose the typer is trying to analyze `p(x)`

The required signature is callable i.e. it has `n` arguments and a return type
as requirement.

    (A,B,...):RT        -- required signature

Now assume that the actual variable at this position is untyped i.e. its type
is a type variable without any constraints.

    TV                  -- actual signature

This type variable can be substituted by a function or a predicate with the
correct number of arguments.

But at this point it might not yet be evident if we substitute the variable by
`(A,B,...)->BOOLEAN` or `(A,B,...)?`. We need a type
(e.g. `@DUMMY[(A,B,...),RT]` which can be downgraded to a predicate or a
function if required. I.e. we add the substitution

    TV ~> @DUMMY[(A,B,...),RT]

In order for this to work some other changes were necessary:

- Introduction of a class `@DUMMY` which serves as a placeholder for
  predicates and functions

- Dependency tracking of type variables: Each type variable gets a list of
  other type variables on which it depends (i.e. which occur in its
  substitution). No circularity is allowed. I.e. If we try to add a
  substitution for some type variable `i` we check that none of the used type
  variables in the substitution depends directly or indirectly on `i`.

- The unifier in the typer has to make the appropriate substitutions:

  - If it encounters a fresh type variable in a callable position it creates a
    dummy type with arguments and result type from the required signature.

  - If it encounters a type variable with a substitution in a callable
    position it downgrades the type in the substitution to a callable
    signature and unifies the callable signature with the required signature.

  - If it encounters a type variable with a callable substitution in a
    position with a required constant signature it verifies that the required
    signature is either a predicate or a function, it unifies the arguments
    and possibly the return type and updates the substitution as a predicate
    or a function type.

- Furthermore the typer has to check the typevariables to not contain dummy
  types at certain positions because this would lead to an incomplete inferred
  type.

	modified:   class_table.ml
	modified:   class_table.mli
	modified:   context.ml
	modified:   context.mli
	modified:   signature.ml
	modified:   typer.ml
Fix: parsing of quantified expressions within proofs

	modified:   class_table.ml
	modified:   parser.mly
Fix: Context.add_consequences_implication

If an implication is added to the context it has to be checked if the
there is either an exact match of the premise or there is a schematic
assertion which can be unified with the premise.

The exact matches have been searched in 'prvd2' which works well only if
the premise is not schematic. If the premise is schematic (i.e. all
quantified) the only way to find an exact match is in 'prvd'.

	modified:   context.ml
	modified:   proof_context.ml
Fix: Termination condition in Term_sub_arr.sub_star

... and replaced a too strong assertion
	modified:   signature.ml
	modified:   typer.ml
Implemented numbers as feature names

Fix: In the typer new untyped type variables are always added at the
bottom and new global type variables (from formal generics of global
features) are always added at the bottom. During unification a newer
type variable can be substituted by an older or a conceptless by a
variable with concept. The other way round is illegal. This order is
enforced now.

	modified:   context.ml
	modified:   parser.mly
	modified:   signature.ml
	modified:   support.ml
	modified:   typer.ml
Fix: Proof is not traced correctly if target is all quantified

	modified:   prover.ml
Fix: Beta reduction in 'term.ml'

After the application of a lambda term its arguments it might be the
case that the reduced term contains again a reducible expression.

	modified:   term.ml
Minor editorial change

	modified:   context.ml
	modified:   feature_table.mli
	modified:   prover.ml
Fix: typing of lambda expressions

- If a lambda expression occurs in a callable position then the
  result type need not be extracted from a compound expression like
  'G?' or 'A->B' but cannot used directly from the result type of
  the signature.

- Expecting a lambda has expected arity = 0

	modified:   class_table.ml
	modified:   typer.ml