The Reprove top-level command

[JimmyZJX]

This PR implements the feature requested by #133.

I refer to the original feature request and comment on my modifications:

The command added to Abella is Reprove, since most of the top-level commands are capitalized.

Check that the last Top-level command was, in fact, Theorem. The reprove keyword should not be allowed immediately following a Definition, for example.

The check is done by a last_top_command variable introduced.

Check that the previous theorem has a completed proof.

The normal behavior of top-level commands is that one cannot invoke during the proof status. I don't check if the last proof was accepted, aborted, or partially skipped.

Reinstate the previous theorem and start reading the following text as a new proof of that theorem.

This is done by re-invoking the last Theorem command.

Example:

Theorem test_reprove : forall (a : o), a = a.
search.
Reprove.
intros. search.
Reprove.
intros. assert a = a. search.