Don't check hostname on network connections to REPL from editors.

It's already restricted to only listening on the 127.0.0.1 interface;
the additional check might just be being paranoid. Doesn't seem like
this kind of thing is a huge security concern, anyways.
Fixes #916.
Think I saw someone else complain about this too, recently.
Fix typo in usage message
Merge pull request #922 from LeifW/dont_check_hostname_in_repl

Don't check hostname on network connections to REPL from editors.
Merge pull request #923 from CodeBlock/patch-1

Fix typo in usage message
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