Correct typing of lambda expressions

Lambda expressions had not been unified with their expected signatures.

A lamda expression can be one of

- quantified expression

- literal predicate

- literal function

In the first case it is sufficient that the type of the inner expression
is a boolean. In the second and third case the upgraded signature (to
a predicate or a function type) has to be unifiable with the expected
signature.

Still to be done: Better error messages and conversion between argument
lists and tuples.

	modified:   ocaml/ast.ml
	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/prover.ml
	modified:   ocaml/signature.ml
	modified:   ocaml/term_builder.ml
	modified:   ocaml/term_builder.mli
	modified:   ocaml/typer.ml
"==>" allowed as alternative implication symbol

	modified:   ocaml/lexer.mll
	modified:   ocaml/support.ml
Disallow predicates, functions and tuples unless the module is used

	modified:   ocaml/class_table.ml
	modified:   ocaml/term_builder.ml
Fix: extraction from tuple corrected

	modified:   ocaml/class_table.ml