Makefile adapted

Added target 'clean' and removed target 'typer' (no longer necessary)

	modified:   ocaml/context.ml
	modified:   ocaml/makefile
Fix: Cumulated argument types missing in 'Local_context'

Local contexts have cumulated argument names but not the corresponding types.
Therefore a local argument is always found in the inner contet, but the type
is taken from the signature which does not contain the type information of
all arguments.

This bug shows up only if we have nested (i.e. more than one) local contexts.

Furthermore the signatures of found global functions are adapted into the local
context. I.e. the index is shifted up appropriately and in the signature there
has to be made space for all formal generics of the local context i.e. between
the formal generics of the global function and the classnames the corresponding
space has to be inserted.

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/context.ml
	modified:   ocaml/typer.ml
Indexing of formal arguments made more natural

If we have a declaration like

    f(a:A, b:B, c:C): RT

the de Bruijn indices of the formal arguments are `a:0, b:1, c:2` which is
more natural than the previous indexing `a:2, b:1, c:0`.

	modified:   ocaml/class_table.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/term.ml
	modified:   ocaml/typer.ml
Removed 'Global_context'

A 'Local_context.t' contains nearly all fields of
'Global_context.t'. Therefore 'Global_context' has been eliminated and all
information is now contained in the local context.

A local context which is empty (i.e. empty signature and no variables) and
contains just the global tables is used as a global context.

Furthermore the module 'Local_context' has been put into an own file because
it might grow.

	modified:   ocaml/class_table.ml
	modified:   ocaml/context.ml
	new file:   ocaml/local_context.ml
	new file:   ocaml/local_context.mli
	modified:   ocaml/prover.ml
	modified:   ocaml/signature.ml
Added implication predefined into the feature table

Since implication is the base of all reasoning it must be included
in the feature table. Nothing should depend on the fact whether
it is defined in the file 'boolean.e' or not.

	modified:   ocaml/assertion_table.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/local_context.ml
	modified:   ocaml/prover.ml
Fix: type variables not updated correctly after the typing of a term

The typing of a term might introduce functions with formal generics.
This implies that type variables which are bound to a constraint are
introduced into the type variables of the type checker. However at
the end of type checking these type variables must be removed,
because they do not belong to the type variables of the context.

Two things can happen if generic functions are used:

a) The formal generics are instantiated with some specific type. This
means that it has to be checked if the specific type satisfies the
constraint.

b) The formal generics can substitute some type variables of the context.
This implies that the free type variables of the context get some
constraints.

Both cases are not yet implemented.

	modified:   ocaml/feature_table.ml
	modified:   ocaml/local_context.ml
Fix: Assertion signature displayed wrongly in case of formal generics

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/context.ml
	modified:   ocaml/local_context.ml
	modified:   ocaml/local_context.mli
	modified:   ocaml/prover.ml
Added an error message

Type inference of formal generics not yet implemented

	modified:   ocaml/local_context.ml
	modified:   ocaml/typer.ml
Adapted module 'Prover' to 'Context'

Adapted the functions in 'prover.ml' so that they use a context and
not the tables directly.

	modified:   ocaml/assertion_table.ml
	modified:   ocaml/assertion_table.mli
	modified:   ocaml/context.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/local_context.ml
	modified:   ocaml/local_context.mli
	modified:   ocaml/prover.ml
Some minor adaptions

- Removed 'Feature_table.implication_chain' and used
  'Term.implication_chain'

- Written a 'Term.implication_chain' which calculates the only
  interesting element. But the function is not yet used

	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/local_ass_context.ml
	modified:   ocaml/prover.ml
	modified:   ocaml/term.ml
Added some builtin functions to the feature table

- @all, @some: to allow quantified expressions
- '()':        to allow predicate application

	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/feature_table.ml
	modified:   ocaml/support.ml