Opaque function annotation

[marcoeilers]

Adds the ability to annotate functions as @opaque(), which will result in the function body not being known by default. The precondition of the function will still aways be checked, and the postcondition of the function is always known.
Individual function applications can then be annotated with @reveal() to reveal the function definition for that specific usage.

Example:

@opaque()
function isGreaterOne(i: Int): Bool
{ i > 1 }

method mDef(j: Int)
    requires j > -50
{
    assume isGreaterOne(j)
    assert j > 1 // fails
}

method mDef2(j: Int)
    requires j > -50
{
    assume @reveal() isGreaterOne(j)
    assert j > 1 // succeeds
}

Internally, applications of opaque functions are encoded using the existing limited version of the function. @reveal() forces the use of the normal version of the function that triggers the definitional axiom.