New evaluation structure used for beta reductions and function expansions

	modified:   ocaml/proof.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
Added 'owner' function to feature table

	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
Changed sequence of trace

	modified:   ocaml/alba.ml
Improved evaluation structure for recursion

The type 'Eval.t' now mimics the structure of 'Term.t' with some
added components to describe evaluations.

The type 'Eval.t' allows to implement full function expansions for
for case that the toplevel function does not have a definition and
is not a boolean function (nor 'all' nor 'some').

	modified:   ocaml/proof.ml
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
Allowed structured subproofs without universal quantification

The following three forms are now allow as structured subproofs:

    require  r1;...
    proof    p1;...
    ensure   e1;... end

    proof    p1;...
    ensure   e1;... end

    require  r1;...
    ensure   e1;... end

Before only the first one has been parsed properly.

	modified:   ocaml/lexer.mll
	modified:   ocaml/parser.mly
Introduced prover strength

With 'strength = 0' the prover does no nested exploration of alternatives.
I.e. it enters the goal explores the alternatives to prove the goal but
during the exploration of an alternative no more alternatives are explored
to prove the premises.

A prover with zero strength is applied to verify interface files.

	modified:   ocaml/ast.ml
	modified:   ocaml/prover.ml