Prover commands for evaluation and typechecking expressions

Now, the prover supports two new commands:

 * :t, :type gives the type of an expression
 * :e, :eval normalises the expression and prints the result

These work within the proof environment, so evaluating expressions that
contain references to hypotheses is allowed.
Merge pull request #924 from david-christiansen/prover-new-commands

Prover commands for evaluation and typechecking expressions