Added support for short definition of functions

There are two ways to define a constant or a function with an expression

First method:

    0:G?
        ensure
            Result = {x:false}
        end

    (<=) (p,q:G?): ghost BOOLEAN
        ensure
            Result = all(x) p(x) => q(x)
        end

Second method:

    0:G? = {x:false}

    (<=) (p,q:G?): ghost BOOLEAN -> all(x) p(x) => q(x)

The second form is in general preferable.

Note: all operators in function definitions have to be put within parentheses
      to avoid ambiguities in the parser

	modified:   ocaml/eiffelc.ml
	modified:   ocaml/parser.mly
	modified:   ocaml/support.ml
Implemented improved focussed expansion

The improved version expands arguments if the function term doesn't
have an expansion.

However the improved version might do a lot of expansions which are
not useful. E.g.

     (not a => false) => not not a
     ~>   (not a => false) => not a => false

because '=>' does not have an expansion. But this is not a useful
expansion.

Therefore the current checking just includes the code but does not
use it. Only function terms can be in the focus and if the function
term does not have an expansion then the whole term does not have an
expansion.

	modified:   ocaml/feature_table.ml