lib: add ML_goal command

Sometimes we want to prove a fact, but the fact is painful or
error-prone to type out manually. In these cases, we'd like to construct
the goal fact using ML and then immediately enter a proof block.

Previously, we could achieve something like this through careful use of
`Thm.trivial` and `schematic_goal`, but this would clutter up the ML
namespace and wouln't handle meta conjuncts (`&&&`). The new `ML_goal`
command addresses both of these issues.

Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>